92 target->source_location = location;
102 t_i->source_location = location;
143 target->make_assignment(
code_assignt(lhs, malloc_expr));
144 target->source_location = location;
162 t_i->source_location = location;
171 t_s->source_location = location;
180 const irept &given_element_type = object_type.
find(ID_C_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);
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))
237 codet array_set(ID_array_set);
238 array_set.copy_to_operands(new_array_data_symbol, zero_element);
240 t_d->make_other(array_set);
241 t_d->source_location = location;
265 t_decl->make_decl(decl);
266 t_decl->source_location = location;
277 sub_java_new.
type() = sub_type;
298 for_body.move_to_operands(init_decl);
303 for_body.move_to_operands(init_subarray);
304 for_body.move_to_operands(assign_subarray);
308 for_loop.
iter() = inc;
309 for_loop.
body() = for_body;
319 return std::prev(next);
331 const auto maybe_code_assign =
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;
Remove Java New Operators.
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
void update()
Update all indices.
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
const exprt & init() const
targett insert_before(const_targett target)
Insertion before the given target.
const codet & body() const
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
void copy_to_operands(const exprt &expr)
Fresh auxiliary symbol creation.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
const componentst & components() const
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
#define CHECK_RETURN(CONDITION)
bool get_bool(const irep_namet &name) const
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct...
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
Templated functions to cast to specific exprt-derived classes.
Expression Initialization.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void compute_location_numbers()
instructionst::iterator targett
symbol_table_baset & symbol_table
A declaration of a local variable.
const exprt & cond() const
Operator to dereference a pointer.
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get(const irep_namet &name) const
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
targett insert_after(const_targett target)
Insertion after the given target.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Base class for tree-like data structures with sharing.
remove_java_newt(symbol_table_baset &symbol_table, message_handlert &_message_handler)
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
The boolean constant false.
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
A generic container class for the GOTO intermediate representation of one function.
message_handlert & get_message_handler()
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.
Base class for all expressions.
The symbol table base class interface.
const source_locationt & source_location() const
const exprt & iter() const
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_programt & goto_program
source_locationt & add_source_location()
bool lower_java_new(goto_programt &)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
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...
Expression to hold a symbol (variable)
Extract class identifier.
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
const typet & subtype() const
An expression containing a side effect.
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
GOTO functions.
void set(const irep_namet &name, const irep_idt &value)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.