cprover
remove_instanceof.cpp File Reference
+ Include dependency graph for remove_instanceof.cpp:

Go to the source code of this file.

Classes

class  remove_instanceoft
 

Functions

static bool contains_instanceof (const exprt &e)
 
void remove_instanceof (goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
 Replace an instanceof in the expression or guard of the passed instruction of the given function body with an explicit class-identifier test. More...
 
void remove_instanceof (goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
 Replace every instanceof in the passed function with an explicit class-identifier test. More...
 
void remove_instanceof (goto_functionst &goto_functions, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
 Replace every instanceof in every function with an explicit class-identifier test. More...
 
void remove_instanceof (goto_modelt &goto_model, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
 Replace every instanceof in every function with an explicit class-identifier test. More...
 

Detailed Description

Remove Instance-of Operators

Definition in file remove_instanceof.cpp.

Function Documentation

◆ contains_instanceof()

static bool contains_instanceof ( const exprt e)
static

Definition at line 174 of file remove_instanceof.cpp.

◆ remove_instanceof() [1/4]

void remove_instanceof ( goto_functionst goto_functions,
symbol_table_baset symbol_table,
const class_hierarchyt class_hierarchy,
message_handlert message_handler 
)

Replace every instanceof in every function with an explicit class-identifier test.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
goto_functionsThe functions to work on.
symbol_tableThe symbol table to add symbols to.
class_hierarchyclass hierarchy analysis of symbol_table
message_handlerlogging output

Definition at line 278 of file remove_instanceof.cpp.

◆ remove_instanceof() [2/4]

void remove_instanceof ( goto_functionst::goto_functiont function,
symbol_table_baset symbol_table,
const class_hierarchyt class_hierarchy,
message_handlert message_handler 
)

Replace every instanceof in the passed function with an explicit class-identifier test.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
functionThe function to work on.
symbol_tableThe symbol table to add symbols to.
class_hierarchyclass hierarchy analysis of symbol_table
message_handlerlogging output

Definition at line 261 of file remove_instanceof.cpp.

◆ remove_instanceof() [3/4]

void remove_instanceof ( goto_modelt goto_model,
const class_hierarchyt class_hierarchy,
message_handlert message_handler 
)

Replace every instanceof in every function with an explicit class-identifier test.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
goto_modelThe functions to work on and the symbol table to add
class_hierarchyclass hierarchy analysis of goto_model's symbol table
message_handlerlogging output symbols to.

Definition at line 300 of file remove_instanceof.cpp.

◆ remove_instanceof() [4/4]

void remove_instanceof ( goto_programt::targett  target,
goto_programt goto_program,
symbol_table_baset symbol_table,
const class_hierarchyt class_hierarchy,
message_handlert message_handler 
)

Replace an instanceof in the expression or guard of the passed instruction of the given function body with an explicit class-identifier test.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
targetThe instruction to work on.
goto_programThe function body containing the instruction.
symbol_tableThe symbol table to add symbols to.
class_hierarchyclass hierarchy analysis of symbol_table
message_handlerlogging output

Definition at line 243 of file remove_instanceof.cpp.