65 if(expr.
id()!=ID_java_instanceof)
75 "java_instanceof should have two operands");
79 check_ptr.type().id()==ID_pointer,
80 "instanceof first operand should be a pointer");
84 target_arg.id()==ID_type,
85 "instanceof second operand should be a type");
86 const typet &target_type=target_arg.type();
90 target_type.id() == ID_struct_tag,
91 "instanceof second operand should have a simple type");
94 std::vector<irep_idt> children=
96 children.push_back(target_name);
100 children.begin(), children.end(), [](
const irep_idt &a,
const irep_idt &b) {
113 "class_identifier_tmp",
121 "instanceof_result_tmp",
142 for(
const auto &clsname : children)
146 or_ops.push_back(test);
155 std::move(else_block));
158 expr = instanceof_result_sym.symbol_expr();
176 if(e.
id() == ID_java_instanceof)
198 if(target->is_target() &&
222 for(goto_programt::instructionst::iterator target=
The type of an expression, extends irept.
void update()
Update all indices.
const irep_idt & get_identifier() const
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.
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.
The null pointer constant.
function_mapt function_map
typet & type()
Return the type of the expression.
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.
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
remove_instanceoft(symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
A constant literal expression.
static bool contains_instanceof(const exprt &e)
reference_typet java_lang_object_type()
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
const irep_idt & id() const
const class_hierarchyt & class_hierarchy
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void compute_location_numbers()
instructionst::iterator targett
A codet representing the declaration of a local variable.
instructionst instructions
The list of instructions in the goto program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
symbol_table_baset & symbol_table
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
The Boolean constant false.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
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.
int compare(const dstringt &b) const
#define Forall_operands(it, expr)
A codet representing sequential composition of program statements.
message_handlert & message_handler
codet representation of an if-then-else statement.
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
idst get_children_trans(const irep_idt &id) const
goto_functionst goto_functions
GOTO functions.
A codet representing an assignment in the program.