63 if(expr.
id()!=ID_java_instanceof)
73 "java_instanceof should have two operands");
77 check_ptr.type().id()==ID_pointer,
78 "instanceof first operand should be a pointer");
82 target_arg.id()==ID_type,
83 "instanceof second operand should be a type");
84 const typet &target_type=target_arg.type();
88 target_type.id()==ID_symbol,
89 "instanceof second operand should have a simple type");
92 std::vector<irep_idt> children=
94 children.push_back(target_name);
111 "class_identifier_tmp",
119 "instanceof_result_tmp",
136 is_null_branch.
cond() =
147 for(
const auto &clsname : children)
151 or_ops.push_back(test);
156 is_null_branch.
else_case() = std::move(else_block);
159 expr = instanceof_result_sym.symbol_expr();
177 if(e.
id() == ID_java_instanceof)
199 if(target->is_target() &&
223 for(goto_programt::instructionst::iterator target=
The type of an expression.
const codet & then_case() const
void update()
Update all indices.
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Remove Instance-of Operators.
Non-graph-based representation of the class hierarchy.
const exprt & cond() const
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
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.
remove_instanceoft(symbol_table_baset &symbol_table, message_handlert &message_handler)
static bool contains_instanceof(const exprt &e)
reference_typet java_lang_object_type()
#define INVARIANT(CONDITION, REASON)
const irep_idt & id() const
void add(const codet &code)
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
A declaration of a local variable.
instructionst instructions
The list of instructions in the goto program.
::goto_functiont goto_functiont
symbol_table_baset & symbol_table
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
The boolean constant false.
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
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.
int compare(const dstringt &b) const
irept & add(const irep_namet &name)
#define Forall_operands(it, expr)
goto_programt & goto_program
class_hierarchyt class_hierarchy
message_handlert & message_handler
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
goto_programt coverage_criteriont message_handlert & message_handler
idst get_children_trans(const irep_idt &id) const
const codet & else_case() const
goto_functionst goto_functions
GOTO functions.
const irep_idt & get_identifier() const