72 std::vector<irep_idt> children =
74 children.push_back(target_type);
79 return a.compare(b) < 0;
83 for(
const auto &class_name : children)
102 const irep_idt &function_identifier,
109 bool changed =
false;
118 "java_instanceof should have two operands");
123 "instanceof first operand should be a pointer");
128 "instanceof second operand should be a type");
132 "instanceof second operand should have a simple type");
190 if(underlying_type ==
jlo)
201 underlying_type.get_identifier(),
205 else if(target_type !=
jlo)
209 target_type.get_identifier(),
240 const irep_idt &function_identifier,
247 target->is_target() &&
255 target->turn_into_skip();
261 function_identifier, target->code_nonconst(), goto_program, target);
265 target->condition_nonconst(),
279 const irep_idt &function_identifier,
283 for(goto_programt::instructionst::iterator target=
307 const irep_idt &function_identifier,
327 const irep_idt &function_identifier,
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Extract class identifier.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Non-graph-based representation of the class hierarchy.
idst get_children_trans(const irep_idt &id) const
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
bool lower_instanceof(const irep_idt &function_identifier, goto_programt &)
Replace every instanceof in the passed function body with an explicit class-identifier test.
message_handlert & message_handler
remove_instanceoft(symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
const class_hierarchyt & class_hierarchy
symbol_table_baset & symbol_table
The symbol table base class interface.
#define Forall_operands(it, expr)
std::pair< typet, std::size_t > java_array_dimension_and_element_type(const struct_tag_typet &type)
Returns the underlying element type and array dimensionality of Java struct type.
exprt get_array_element_type_field(const exprt &pointer)
exprt get_array_dimension_field(const exprt &pointer)
java_reference_typet java_lang_object_type()
#define JAVA_REFERENCE_ARRAY_CLASSID
bool can_cast_type< java_reference_typet >(const typet &type)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static exprt subtype_expr(const exprt &classid_field, const irep_idt &target_type, const class_hierarchyt &class_hierarchy)
Produce an expression of the form classid_field == "A" || classid_field == "B" || ....
static bool contains_instanceof(const exprt &e)
void remove_instanceof(const irep_idt &function_identifier, 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...
Remove Instance-of Operators.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.