Go to the documentation of this file.
125 const irep_idt &function_identifier,
173 const auto underlying_type_and_dimension =
176 bool target_type_is_reference_array =
177 underlying_type_and_dimension.second >= 1 &&
180 if(target_type_is_reference_array)
186 object_array_dimension,
188 underlying_type_and_dimension.second, object_array_dimension.
type()),
195 object_array_element_type,
220 const irept &given_element_type = object_type.
find(ID_element_type);
221 typet allocate_data_type;
228 allocate_data_type =
data.type();
231 ID_java_new_array_data, allocate_data_type, location);
238 const irept size_bound = rhs.
find(ID_length_upper_bound);
242 data_java_new_expr.
set(ID_size, size_bound);
248 data_java_new_expr.
type(),
249 "tmp_new_data_array",
260 code_assignt(new_array_data_symbol, data_java_new_expr), location));
262 exprt cast_java_new = new_array_data_symbol;
263 if(cast_java_new.
type() !=
data.type())
271 if(!rhs.
get_bool(ID_skip_initialize))
273 const auto zero_element =
276 codet array_set(ID_array_set);
307 sub_java_new.
type() = sub_type;
316 sub_type,
"subarray_init", location, function_identifier,
symbol_table)
320 for_body.
add(std::move(init_decl));
323 for_body.
add(std::move(init_subarray));
326 for_body.
add(std::move(assign_subarray));
343 return std::prev(next);
353 const irep_idt &function_identifier,
357 if(!target->is_assign())
360 if(
as_const(*target).get_assign().rhs().id() == ID_side_effect)
364 const auto code_assign = target->get_assign();
366 const exprt &lhs = code_assign.lhs();
367 const exprt &rhs = code_assign.rhs();
370 const auto &statement = side_effect_expr.get_statement();
372 if(statement == ID_java_new)
375 function_identifier, lhs, side_effect_expr, goto_program, target);
377 else if(statement == ID_java_new_array)
380 function_identifier, lhs, side_effect_expr, goto_program, target);
394 const irep_idt &function_identifier,
397 bool changed =
false;
398 for(goto_programt::instructionst::iterator target =
405 changed = changed || new_target == target;
423 const irep_idt &function_identifier,
441 const irep_idt &function_identifier,
462 bool changed =
false;
Class that provides messages with a built-in verbosity 'level'.
remove_java_newt(symbol_table_baset &symbol_table, message_handlert &_message_handler)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
const irep_idt & get_identifier() const
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool can_cast_type< java_reference_typet >(const typet &type)
A codet representing sequential composition of program statements.
const typet & subtype() const
bool lower_java_new(const irep_idt &function_identifier, goto_programt &)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
exprt get_array_dimension_field(const exprt &pointer)
codet representation of a for statement.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Operator to dereference a pointer.
const irept & find(const irep_namet &name) const
void update()
Update all indices.
A codet representing the declaration of a local variable.
The plus expression Associativity is not specified.
void compute_location_numbers()
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Base class for all expressions.
A struct tag type, i.e., struct_typet with an identifier.
side_effect_exprt & to_side_effect_expr(exprt &expr)
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
symbol_table_baset & symbol_table
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Expression Initialization.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
#define PRECONDITION(CONDITION)
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
pointer_typet pointer_type(const typet &subtype)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void add(const codet &code)
The Boolean constant false.
void remove_java_new(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
goto_programt::targett lower_java_new_array(const irep_idt &function_identifier, const exprt &lhs, const side_effect_exprt &rhs, goto_programt &, goto_programt::targett)
Replaces the instruction lhs = new java_array_type by the following code: lhs = ALLOCATE(java_type) l...
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
::goto_functiont goto_functiont
Extract member of struct or union.
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
message_handlert & get_message_handler()
Structure type, corresponds to C style structs.
goto_functionst goto_functions
GOTO functions.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set(const irep_namet &name, const irep_idt &value)
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Templated functions to cast to specific exprt-derived classes.
A generic container class for the GOTO intermediate representation of one function.
Extract class identifier.
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
std::pair< typet, std::size_t > java_array_dimension_and_element_type(const struct_tag_typet &type)
Returns the underlying element type and array dimensionality of Java struct type.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Remove Java New Operators.
source_locationt & add_source_location()
Semantic type conversion.
exprt get_array_element_type_field(const exprt &pointer)
A codet representing an assignment in the program.
A constant literal expression.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
instructionst::iterator targett
An expression containing a side effect.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Data structure for representing an arbitrary statement in a program.