Go to the documentation of this file.
9 #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
10 #define CPROVER_UTIL_ALLOCATE_OBJECTS_H
48 const exprt &target_expr,
49 const typet &allocate_type,
51 const irep_idt &basename_prefix =
"tmp");
55 const exprt &target_expr,
56 const typet &allocate_type,
57 const irep_idt &basename_prefix =
"tmp");
61 const exprt &target_expr,
62 const typet &allocate_type,
63 const irep_idt &basename_prefix =
"tmp");
82 const exprt &target_expr,
83 const typet &allocate_type);
90 const exprt &target_expr,
91 const typet &allocate_type);
94 const typet &allocate_type,
95 const irep_idt &basename_prefix =
"tmp");
115 const exprt &target_expr,
116 const typet &allocate_type,
117 const bool static_lifetime,
127 #endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
The type of an expression, extends irept.
void add_created_symbol(const symbolt *symbol_ptr)
Add a pointer to a symbol to the list of pointers to symbols created so far.
Base class for all expressions.
symbol_table_baset & symbol_table
Expression to hold a symbol (variable)
Defines typet, type_with_subtypet and type_with_subtypest.
const irep_idt symbol_mode
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< const symbolt * > symbols_created
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a dynamic object.
The symbol table base class interface.
exprt allocate_static_global_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a global variable with static lifetime.
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
allocate_objectst(const irep_idt &symbol_mode, const source_locationt &source_location, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
const irep_idt name_prefix
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
lifetimet
Selects the kind of objects allocated.
const source_locationt source_location
exprt allocate_non_dynamic_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const bool static_lifetime, const irep_idt &basename_prefix)
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
exprt allocate_dynamic_object(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that derefer...
void mark_created_symbols_as_input(code_blockt &init_code)
Adds code to mark the created symbols as input.
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
A codet representing an assignment in the program.