16 const exprt &array_length_expr,
20 const auto &element_type =
24 ID_java_new_array, {array_length_expr},
pointer_type, loc};
53 auto ptr = std::make_shared<code_without_referencest>(std::move(code));
54 list.emplace_back(std::move(ptr));
64 auto ptr = std::make_shared<reference_allocationt>(std::move(ref));
65 list.emplace_back(std::move(ptr));
75 auto ptr = std::make_shared<code_without_referencest>(std::move(code));
76 list.emplace_front(std::move(ptr));
pointer_typet pointer_type(const typet &subtype)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
void add(const codet &code)
A codet representing an assignment in the program.
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
void add_to_front(code_without_referencest code)
std::list< std::shared_ptr< code_with_referencest > > list
void append(code_with_references_listt &&other)
void add(code_without_referencest code)
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Code that should not contain reference.
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
typet & type()
Return the type of the expression.
void set(const irep_idt &name, const irep_idt &value)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Allocation code which contains a reference.
code_blockt to_code(reference_substitutiont &references) const override
A side_effect_exprt that returns a non-deterministically chosen value.
An expression containing a side effect.
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.
signedbv_typet java_int_type()
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool can_cast_expr< constant_exprt >(const exprt &base)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Information to store when several references point to the same Java object.
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.
optionalt< exprt > array_length
If symbol is an array, this expression stores its length.