CBMC
allocate_objects.h File Reference
#include <util/namespace.h>
#include <util/std_code.h>
+ Include dependency graph for allocate_objects.h:
+ This graph shows which files directly or indirectly include this file:

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...
 

Enumeration Type Documentation

◆ lifetimet

enum lifetimet
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.

Function Documentation

◆ make_allocate_code()

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

Parameters
lhspointer which will be allocated
sizesize of the object
Returns
code allocating the object and assigning it to lhs

Definition at line 261 of file allocate_objects.cpp.