cprover
|
Public Member Functions | |
remove_instanceoft (symbol_table_baset &symbol_table, message_handlert &message_handler) | |
bool | lower_instanceof (goto_programt &) |
Replace every instanceof in the passed function body with an explicit class-identifier test. More... | |
bool | lower_instanceof (goto_programt &, goto_programt::targett) |
Replaces expressions like e instanceof A with e. More... | |
Protected Member Functions | |
bool | lower_instanceof (exprt &, goto_programt &, goto_programt::targett) |
Replaces an expression like e instanceof A with e. More... | |
Protected Attributes | |
symbol_table_baset & | symbol_table |
namespacet | ns |
class_hierarchyt | class_hierarchy |
message_handlert & | message_handler |
Definition at line 23 of file remove_instanceof.cpp.
|
inline |
Definition at line 26 of file remove_instanceof.cpp.
References class_hierarchy, and symbol_table.
bool remove_instanceoft::lower_instanceof | ( | goto_programt & | goto_program | ) |
Replace every instanceof in the passed function body with an explicit class-identifier test.
Extra auxiliary variables may be introduced into symbol_table.
goto_program | The function body to work on. |
Definition at line 220 of file remove_instanceof.cpp.
References goto_program, goto_programt::instructions, and goto_programt::update().
Referenced by lower_instanceof(), and remove_instanceof().
bool remove_instanceoft::lower_instanceof | ( | goto_programt & | goto_program, |
goto_programt::targett | target | ||
) |
Replaces expressions like e instanceof A with e.
@class_identifier == "A" or a big-or of similar expressions if we know of subtypes that also satisfy the given test. Does this for the code or guard at a specific instruction.
goto_program | program to process |
target | instruction to check for instanceof expressions |
Definition at line 195 of file remove_instanceof.cpp.
References contains_instanceof(), goto_program, goto_programt::insert_before_swap(), and lower_instanceof().
|
protected |
Replaces an expression like e instanceof A with e.
@class_identifier == "A" or a big-or of similar expressions if we know of subtypes that also satisfy the given test.
expr | Expression to lower (the code or the guard of an instruction) |
goto_program | program the expression belongs to |
this_inst | instruction the expression is found at |
Definition at line 58 of file remove_instanceof.cpp.
References code_blockt::add(), irept::add(), class_hierarchy, dstringt::compare(), code_ifthenelset::cond(), goto_programt::destructive_insert(), disjunction(), code_ifthenelset::else_case(), Forall_operands, class_hierarchyt::get_children_trans(), get_class_identifier_field(), get_fresh_aux_symbol(), symbol_typet::get_identifier(), goto_convert(), goto_program, irept::id(), id2string(), INVARIANT, java_lang_object_type(), lower_instanceof(), message_handler, ns, exprt::op0(), exprt::op1(), exprt::operands(), symbolt::symbol_expr(), symbol_table, code_ifthenelset::then_case(), to_pointer_type(), to_symbol_type(), and exprt::type().
|
protected |
Definition at line 44 of file remove_instanceof.cpp.
Referenced by lower_instanceof(), and remove_instanceoft().
|
protected |
Definition at line 45 of file remove_instanceof.cpp.
Referenced by lower_instanceof().
|
protected |
Definition at line 43 of file remove_instanceof.cpp.
Referenced by lower_instanceof().
|
protected |
Definition at line 42 of file remove_instanceof.cpp.
Referenced by lower_instanceof(), and remove_instanceoft().