|
CBMC
|
#include "allocate_objects.h"#include <util/c_types.h>#include <util/fresh_symbol.h>#include <util/pointer_expr.h>#include <util/pointer_offset_size.h>#include <util/symbol.h>#include "goto_instruction_code.h"
Include dependency graph for allocate_objects.cpp:Go to the source code of this file.
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... | |
| 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.