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

Public Member Functions

 remove_instanceoft (symbol_table_baset &symbol_table)
 
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

std::size_t 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
 

Detailed Description

Definition at line 22 of file remove_instanceof.cpp.

Constructor & Destructor Documentation

◆ remove_instanceoft()

remove_instanceoft::remove_instanceoft ( symbol_table_baset symbol_table)
inlineexplicit

Definition at line 25 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 165 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 145 of file remove_instanceof.cpp.

References goto_program, and lower_instanceof().

◆ lower_instanceof() [3/3]

std::size_t 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
number of instanceof expressions that have been replaced

Definition at line 53 of file remove_instanceof.cpp.

References class_hierarchy, dstringt::compare(), disjunction(), Forall_operands, class_hierarchyt::get_children_trans(), get_class_identifier_field(), get_fresh_aux_symbol(), symbol_typet::get_identifier(), goto_program, irept::id(), id2string(), goto_programt::insert_after(), INVARIANT, java_lang_object_type(), lower_instanceof(), ns, exprt::op0(), exprt::op1(), exprt::operands(), exprt::source_location(), symbolt::symbol_expr(), symbol_table, to_pointer_type(), to_symbol_type(), and exprt::type().

Member Data Documentation

◆ class_hierarchy

class_hierarchyt remove_instanceoft::class_hierarchy
protected

Definition at line 40 of file remove_instanceof.cpp.

Referenced by lower_instanceof(), and remove_instanceoft().

◆ ns

namespacet remove_instanceoft::ns
protected

Definition at line 39 of file remove_instanceof.cpp.

Referenced by lower_instanceof().

◆ symbol_table

symbol_table_baset& remove_instanceoft::symbol_table
protected

Definition at line 38 of file remove_instanceof.cpp.

Referenced by lower_instanceof(), and remove_instanceoft().


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