cprover
remove_instanceoft Class Reference
Collaboration diagram for remove_instanceoft:
[legend]

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_basetsymbol_table
 
namespacet ns
 
class_hierarchyt class_hierarchy
 
message_handlertmessage_handler
 

Detailed Description

Definition at line 23 of file remove_instanceof.cpp.

Constructor & Destructor Documentation

◆ remove_instanceoft()

remove_instanceoft::remove_instanceoft ( symbol_table_baset symbol_table,
message_handlert message_handler 
)
inline

Definition at line 26 of file remove_instanceof.cpp.

References class_hierarchy, and symbol_table.

Member Function Documentation

◆ lower_instanceof() [1/3]

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.

Parameters
goto_programThe function body to work on.
Returns
true if one or more instanceof expressions have been replaced

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().

◆ lower_instanceof() [2/3]

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.

Parameters
goto_programprogram to process
targetinstruction to check for instanceof expressions
Returns
true if an instanceof has been replaced

Definition at line 195 of file remove_instanceof.cpp.

References contains_instanceof(), goto_program, goto_programt::insert_before_swap(), and lower_instanceof().

◆ lower_instanceof() [3/3]

bool remove_instanceoft::lower_instanceof ( exprt expr,
goto_programt goto_program,
goto_programt::targett  this_inst 
)
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.

Parameters
exprExpression to lower (the code or the guard of an instruction)
goto_programprogram the expression belongs to
this_instinstruction the expression is found at
Returns
true if any instanceof instructionw was replaced

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().

Member Data Documentation

◆ class_hierarchy

class_hierarchyt remove_instanceoft::class_hierarchy
protected

Definition at line 44 of file remove_instanceof.cpp.

Referenced by lower_instanceof(), and remove_instanceoft().

◆ message_handler

message_handlert& remove_instanceoft::message_handler
protected

Definition at line 45 of file remove_instanceof.cpp.

Referenced by lower_instanceof().

◆ ns

namespacet remove_instanceoft::ns
protected

Definition at line 43 of file remove_instanceof.cpp.

Referenced by lower_instanceof().

◆ symbol_table

symbol_table_baset& remove_instanceoft::symbol_table
protected

Definition at line 42 of file remove_instanceof.cpp.

Referenced by lower_instanceof(), and remove_instanceoft().


The documentation for this class was generated from the following file: