Go to the documentation of this file.
15 const exprt &array_length_expr,
19 const auto &element_type =
22 java_new_array.copy_to_operands(array_length_expr);
23 java_new_array.type().
subtype().
set(ID_element_type, element_type);
52 auto ptr = std::make_shared<code_without_referencest>(std::move(code));
53 list.emplace_back(std::move(ptr));
63 auto ptr = std::make_shared<reference_allocationt>(std::move(ref));
64 list.emplace_back(std::move(ptr));
74 auto ptr = std::make_shared<code_without_referencest>(std::move(code));
75 list.emplace_front(std::move(ptr));
void add(code_without_referencest code)
A codet representing sequential composition of program statements.
const typet & subtype() const
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.
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
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.
Base class for all expressions.
void add_to_front(code_without_referencest code)
typet & type()
Return the type of the expression.
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.
Code that should not contain reference.
Allocation code which contains a reference.
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.
pointer_typet pointer_type(const typet &subtype)
Information to store when several references point to the same Java object.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void add(const codet &code)
signedbv_typet java_int_type()
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< exprt > array_length
If symbol is an array, this expression stores its length.
A side_effect_exprt that returns a non-deterministically chosen value.
void append(code_with_references_listt &&other)
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
std::list< std::shared_ptr< code_with_referencest > > list
void set(const irep_namet &name, const irep_idt &value)
bool can_cast_expr< constant_exprt >(const exprt &base)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A codet representing an assignment in the program.
An expression containing a side effect.
code_blockt to_code(reference_substitutiont &references) const override
Data structure for representing an arbitrary statement in a program.