CBMC
code_with_references.cpp File Reference
#include "code_with_references.h"
#include "java_types.h"
#include <util/arith_tools.h>
+ 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. 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.