|
CBMC
|
Include dependency graph for code_with_references.cpp:Go to the source code of this file.
Functions | |
| codet | allocate_array (const exprt &expr, const exprt &array_length_expr, const source_locationt &loc) |
Allocate a fresh array of length array_length_expr and assigns expr to it. | |
| codet allocate_array | ( | const exprt & | expr, |
| const exprt & | array_length_expr, | ||
| const source_locationt & | loc | ||
| ) |
Allocate a fresh array of length array_length_expr and assigns expr to it.
Definition at line 14 of file code_with_references.cpp.