Go to the documentation of this file.
92 target->source_location = location;
101 t_i->make_assignment(
code_assignt(deref, *zero_object));
102 t_i->source_location = location;
143 target->make_assignment(
code_assignt(lhs, malloc_expr));
144 target->source_location = location;
161 t_i->make_assignment(
code_assignt(deref, *zero_object));
162 t_i->source_location = location;
171 t_s->source_location = location;
180 const irept &given_element_type = object_type.
find(ID_element_type);
181 typet allocate_data_type;
182 if(given_element_type.is_not_nil())
185 pointer_type(static_cast<const typet &>(given_element_type));
188 allocate_data_type =
data.type();
191 ID_java_new_array_data, allocate_data_type, location);
198 const irept size_bound = rhs.
find(ID_length_upper_bound);
200 data_java_new_expr.
set(ID_size, rhs.
op0());
202 data_java_new_expr.
set(ID_size, size_bound);
208 data_java_new_expr.
type(),
210 "tmp_new_data_array",
218 t_array_decl->make_decl(array_decl);
219 t_array_decl->source_location = location;
221 t_p2->make_assignment(
222 code_assignt(new_array_data_symbol, data_java_new_expr));
223 t_p2->source_location = location;
226 exprt cast_java_new = new_array_data_symbol;
227 if(cast_java_new.
type() !=
data.type())
233 if(!rhs.
get_bool(ID_skip_initialize))
235 const auto zero_element =
238 codet array_set(ID_array_set);
239 array_set.copy_to_operands(new_array_data_symbol, *zero_element);
241 t_d->make_other(array_set);
242 t_d->source_location = location;
266 t_decl->make_decl(decl);
267 t_decl->source_location = location;
274 static_cast<const typet &>(rhs.
type().
subtype().
find(ID_element_type));
276 sub_java_new.
type() = sub_type;
297 for_body.
add(std::move(init_decl));
300 for_body.add(std::move(init_subarray));
303 for_body.add(std::move(assign_subarray));
309 std::move(for_body));
319 return std::prev(next);
331 const auto maybe_code_assign =
332 expr_try_dynamic_cast<code_assignt>(target->code);
333 if(!maybe_code_assign)
336 const exprt &lhs = maybe_code_assign->lhs();
337 const exprt &rhs = maybe_code_assign->rhs();
339 if(rhs.
id() == ID_side_effect && rhs.
get(ID_statement) == ID_java_new)
344 if(rhs.
id() == ID_side_effect && rhs.
get(ID_statement) == ID_java_new_array)
360 bool changed =
false;
361 for(goto_programt::instructionst::iterator target =
367 changed = changed || new_target == target;
420 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 componentst & components() const
A codet representing sequential composition of program statements.
#define PRECONDITION(CONDITION)
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
codet representation of a for statement.
The type of an expression, extends irept.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Operator to dereference a pointer.
irept & add(const irep_namet &name)
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()
Base class for all expressions.
side_effect_exprt & to_side_effect_expr(exprt &expr)
function_mapt function_map
Expression to hold a symbol (variable)
symbol_table_baset & symbol_table
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.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
exprt size_of_expr(const typet &type, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool lower_java_new(goto_programt &)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
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.
The Boolean constant false.
void remove_java_new(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_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.
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
A base class for relations, i.e., binary predicates.
Templated functions to cast to specific exprt-derived classes.
A generic container class for the GOTO intermediate representation of one function.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Base class for tree-like data structures with sharing.
source_locationt & add_source_location()
Semantic type conversion.
A codet representing an assignment in the program.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
goto_programt::targett lower_java_new_array(exprt lhs, 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...
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.
#define CHECK_RETURN(CONDITION)