9#ifndef CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
10#define CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
19 const exprt &array_length_expr,
95 std::list<std::shared_ptr<code_with_referencest>>
list;
A codet representing sequential composition of program statements.
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)
Base class for code which can contain references which can get replaced before generating actual code...
virtual ~code_with_referencest()=default
virtual code_blockt to_code(reference_substitutiont &) const =0
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Code that should not contain reference.
code_without_referencest(codet code)
code_blockt to_code(reference_substitutiont &) const override
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
Allocation code which contains a reference.
reference_allocationt(std::string reference_id, source_locationt loc)
code_blockt to_code(reference_substitutiont &references) const override
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.
nonstd::optional< T > optionalt
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.