CBMC
|
Go to the source code of this file.
Classes | |
class | allocate_objectst |
Enumerations | |
enum class | lifetimet { AUTOMATIC_LOCAL , STATIC_GLOBAL , DYNAMIC } |
Selects the kind of objects allocated. More... | |
Functions | |
code_frontend_assignt | make_allocate_code (const symbol_exprt &lhs, const exprt &size) |
Create code allocating an object of size size and assigning it to lhs More... | |
|
strong |
Selects the kind of objects allocated.
Enumerator | |
---|---|
AUTOMATIC_LOCAL | Allocate local objects with automatic lifetime. |
STATIC_GLOBAL | Allocate global objects with static lifetime. |
DYNAMIC | Allocate dynamic objects (using ALLOCATE) |
Definition at line 16 of file allocate_objects.h.
code_frontend_assignt make_allocate_code | ( | const symbol_exprt & | lhs, |
const exprt & | size | ||
) |
Create code allocating an object of size size
and assigning it to lhs
lhs | pointer which will be allocated |
size | size of the object |
lhs
Definition at line 261 of file allocate_objects.cpp.