Include dependency graph for code_with_references.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| struct | object_creation_referencet |
| Information to store when several references point to the same Java object. More... | |
| class | code_with_referencest |
| Base class for code which can contain references which can get replaced before generating actual codet. More... | |
| class | code_without_referencest |
| Code that should not contain reference. More... | |
| class | reference_allocationt |
| Allocation code which contains a reference. More... | |
| class | code_with_references_listt |
| Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer interface. More... | |
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. More... | |
Function Documentation
◆ allocate_array()
| 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.
