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

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_tabletsymbol_table
 
namespacet ns
 
class_hierarchyt class_hierarchy
 
goto_functionstgoto_functions
 

Detailed Description

Definition at line 21 of file remove_instanceof.cpp.

Member Typedef Documentation

§ instanceof_instt

Definition at line 46 of file remove_instanceof.cpp.

Constructor & Destructor Documentation

§ remove_instanceoft()

remove_instanceoft::remove_instanceoft ( symbol_tablet _symbol_table,
goto_functionst _goto_functions 
)
inline

Definition at line 24 of file remove_instanceof.cpp.

References class_hierarchy, and lower_instanceof().

Member Function Documentation

§ contains_instanceof()

bool remove_instanceoft::contains_instanceof ( const exprt expr)
protected

Avoid breaking sharing by checking for instanceof before calling lower_instanceof.

parameters: Expression expr
Returns
Returns true if expr contains any instanceof ops

Definition at line 66 of file remove_instanceof.cpp.

References forall_operands, and irept::id().

Referenced by lower_instanceof().

§ lower_instanceof() [1/4]

void remove_instanceoft::lower_instanceof ( )

See function above.

Returns
Side-effects on this->goto_functions, replacing every instanceof in every function with an explicit test.

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

§ lower_instanceof() [2/4]

bool remove_instanceoft::lower_instanceof ( goto_programt goto_program)
protected

See function above.

parameters: goto_program, all of whose instanceof expressions will
be replaced by explicit class-identifier tests.
Returns
Side-effect on 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().

§ lower_instanceof() [3/4]

void remove_instanceoft::lower_instanceof ( goto_programt goto_program,
goto_programt::targett  target,
instanceof_instt inst_switch 
)
protected

See function above.

parameters: GOTO program instruction target whose instanceof
expressions, if any, should be replaced with explicit tests, and the goto_program it is part of.
Returns
Side-effect on target as above.

Definition at line 156 of file remove_instanceof.cpp.

References contains_instanceof(), and lower_instanceof().

§ lower_instanceof() [4/4]

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

parameters: Expression to lower expr and the goto_program and
instruction this_inst it belongs to.
Returns
Side-effect on 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().

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

§ goto_functions

goto_functionst& remove_instanceoft::goto_functions
protected

Definition at line 41 of file remove_instanceof.cpp.

Referenced by lower_instanceof().

§ ns

namespacet remove_instanceoft::ns
protected

Definition at line 39 of file remove_instanceof.cpp.

Referenced by lower_instanceof().

§ symbol_table

symbol_tablet& remove_instanceoft::symbol_table
protected

Definition at line 38 of file remove_instanceof.cpp.

Referenced by lower_instanceof().


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