cprover
|
Remove Instance-of Operators. More...
#include "remove_instanceof.h"
#include <goto-programs/class_hierarchy.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_convert.h>
#include <util/fresh_symbol.h>
#include <java_bytecode/java_types.h>
#include <sstream>
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... | |
Remove Instance-of Operators.
Definition in file remove_instanceof.cpp.
|
static |
Definition at line 174 of file remove_instanceof.cpp.
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.
target | The instruction to work on. |
goto_program | The function body containing the instruction. |
symbol_table | The symbol table to add symbols to. |
class_hierarchy | class hierarchy analysis of symbol_table |
message_handler | logging output |
Definition at line 243 of file remove_instanceof.cpp.
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.
function | The function to work on. |
symbol_table | The symbol table to add symbols to. |
class_hierarchy | class hierarchy analysis of symbol_table |
message_handler | logging output |
Definition at line 261 of file remove_instanceof.cpp.
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.
goto_functions | The functions to work on. |
symbol_table | The symbol table to add symbols to. |
class_hierarchy | class hierarchy analysis of symbol_table |
message_handler | logging output |
Definition at line 278 of file remove_instanceof.cpp.
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.
goto_model | The functions to work on and the symbol table to add |
class_hierarchy | class hierarchy analysis of goto_model's symbol table |
message_handler | logging output symbols to. |
Definition at line 300 of file remove_instanceof.cpp.