58 if(expr.
id()!=ID_java_instanceof)
60 std::size_t replacements=0;
68 "java_instanceof should have two operands");
72 check_ptr.type().id()==ID_pointer,
73 "instanceof first operand should be a pointer");
77 target_arg.id()==ID_type,
78 "instanceof second operand should be a type");
79 const typet &target_type=target_arg.type();
83 target_type.id()==ID_symbol,
84 "instanceof second operand should have a simple type");
87 std::vector<irep_idt> children=
89 children.push_back(target_name);
116 newinst->make_assignment();
119 newinst->function=this_inst->function;
128 for(
const auto &clsname : children)
132 or_ops.push_back(test);
149 std::size_t replacements=
156 target->swap(*std::next(target, replacements));
168 for(goto_programt::instructionst::iterator target=
The type of an expression.
void update()
Update all indices.
const std::string & id2string(const irep_idt &d)
Remove Instance-of Operators.
remove_instanceoft(symbol_table_baset &symbol_table)
Fresh auxiliary symbol creation.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
function_mapt function_map
bool lower_instanceof(goto_programt &)
Replace every instanceof in the passed function body with an explicit class-identifier test...
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
reference_typet java_lang_object_type()
#define INVARIANT(CONDITION, REASON)
const irep_idt & id() const
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void compute_location_numbers()
A reference into the symbol table.
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
::goto_functiont goto_functiont
symbol_table_baset & symbol_table
targett insert_after(const_targett target)
Insertion after the given target.
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
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
int compare(const dstringt &b) const
#define Forall_operands(it, expr)
goto_programt & goto_program
class_hierarchyt class_hierarchy
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
idst get_children_trans(const irep_idt &id) const
goto_functionst goto_functions
GOTO functions.
const irep_idt & get_identifier() const