69 if(expr.
id()==ID_java_instanceof)
89 if(expr.
id()==ID_java_instanceof)
92 assert(check_ptr.
type().
id()==ID_pointer);
94 assert(target_arg.id()==ID_type);
95 const typet &target_type=target_arg.type();
98 assert(target_type.id()==ID_symbol);
101 std::vector<irep_idt> children=
103 children.push_back(target_name);
105 assert(!children.empty() &&
"Unable to execute instanceof");
124 newinst->make_assignment();
132 inst_switch.push_back(make_pair(this_inst, newinst));
135 for(
const auto &clsname : children)
139 or_ops.push_back(test);
169 assert(!(code_iof && guard_iof));
185 if(!inst_switch.empty())
187 for(
auto &p : inst_switch)
191 this_inst->swap(*newinst);
void lower_instanceof()
See function above.
The type of an expression.
void update()
Update all indices.
Remove Instance-of Operators.
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Fresh auxiliary symbol creation.
bool contains_instanceof(const exprt &)
Avoid breaking sharing by checking for instanceof before calling lower_instanceof.
symbol_tablet 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.
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
void compute_location_numbers()
A reference into the symbol table.
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
#define forall_operands(it, expr)
goto_functionst & goto_functions
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)
function_mapt function_map
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
symbol_tablet & symbol_table
Base class for all expressions.
std::vector< std::pair< goto_programt::targett, goto_programt::targett > > instanceof_instt
const source_locationt & source_location() const
remove_instanceoft(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
#define Forall_operands(it, expr)
class_hierarchyt class_hierarchy
#define Forall_goto_program_instructions(it, program)
Extract class identifier.
idst get_children_trans(const irep_idt &id) const
goto_functionst goto_functions
const irep_idt & get_identifier() const
instructionst::iterator targett