cprover
|
Public Member Functions | |
remove_instanceoft (symbol_tablet &_symbol_table, goto_functionst &_goto_functions) | |
void | lower_instanceof () |
See function above. More... | |
Protected Types | |
typedef std::vector< std::pair< goto_programt::targett, goto_programt::targett > > | instanceof_instt |
Protected Member Functions | |
bool | lower_instanceof (goto_programt &) |
See function above. More... | |
void | lower_instanceof (goto_programt &, goto_programt::targett, instanceof_instt &) |
See function above. More... | |
void | lower_instanceof (exprt &, goto_programt &, goto_programt::targett, instanceof_instt &) |
Replaces an expression like e instanceof A with e. More... | |
bool | contains_instanceof (const exprt &) |
Avoid breaking sharing by checking for instanceof before calling lower_instanceof. More... | |
Protected Attributes | |
symbol_tablet & | symbol_table |
namespacet | ns |
class_hierarchyt | class_hierarchy |
goto_functionst & | goto_functions |
Definition at line 21 of file remove_instanceof.cpp.
|
protected |
Definition at line 46 of file remove_instanceof.cpp.
|
inline |
Definition at line 24 of file remove_instanceof.cpp.
References class_hierarchy, and lower_instanceof().
|
protected |
Avoid breaking sharing by checking for instanceof before calling lower_instanceof.
expr
contains any instanceof ops Definition at line 66 of file remove_instanceof.cpp.
References forall_operands, and irept::id().
Referenced by lower_instanceof().
void remove_instanceoft::lower_instanceof | ( | ) |
See function above.
Definition at line 203 of file remove_instanceof.cpp.
References goto_functions_templatet< bodyT >::compute_location_numbers(), goto_functions_templatet< bodyT >::function_map, and goto_functions.
Referenced by lower_instanceof(), remove_instanceof(), and remove_instanceoft().
|
protected |
See function above.
goto_program
as above. Definition at line 180 of file remove_instanceof.cpp.
References Forall_goto_program_instructions, lower_instanceof(), and goto_program_templatet< codeT, guardT >::update().
|
protected |
See function above.
goto_program
it is part of. target
as above. Definition at line 156 of file remove_instanceof.cpp.
References contains_instanceof(), and lower_instanceof().
|
protected |
Replaces an expression like e instanceof A with e.
== "A" Or a big-or of similar expressions if we know of subtypes that also satisfy the given test.
this_inst
it belongs to. expr
replacing it with an explicit clsid test Definition at line 83 of file remove_instanceof.cpp.
References class_hierarchy, disjunction(), Forall_operands, class_hierarchyt::get_children_trans(), get_class_identifier_field(), get_fresh_aux_symbol(), symbol_typet::get_identifier(), irept::id(), goto_program_templatet< codeT, guardT >::insert_after(), lower_instanceof(), ns, exprt::op0(), exprt::op1(), exprt::source_location(), symbolt::symbol_expr(), symbol_table, to_symbol_type(), and exprt::type().
|
protected |
Definition at line 40 of file remove_instanceof.cpp.
Referenced by lower_instanceof(), and remove_instanceoft().
|
protected |
Definition at line 41 of file remove_instanceof.cpp.
Referenced by lower_instanceof().
|
protected |
Definition at line 39 of file remove_instanceof.cpp.
Referenced by lower_instanceof().
|
protected |
Definition at line 38 of file remove_instanceof.cpp.
Referenced by lower_instanceof().