cprover
remove_instanceof.cpp File Reference

Remove Instance-of Operators. More...

#include "remove_instanceof.h"
#include "class_hierarchy.h"
#include "class_identifier.h"
#include <util/fresh_symbol.h>
#include <sstream>
Include dependency graph for remove_instanceof.cpp:

Go to the source code of this file.

Classes

class  remove_instanceoft
 

Functions

void remove_instanceof (symbol_tablet &symbol_table, goto_functionst &goto_functions)
 See function above. More...
 
void remove_instanceof (goto_modelt &goto_model)
 

Detailed Description

Remove Instance-of Operators.

Definition in file remove_instanceof.cpp.

Function Documentation

◆ remove_instanceof() [1/2]

void remove_instanceof ( symbol_tablet symbol_table,
goto_functionst goto_functions 
)

See function above.

parameters: goto_functions, a function map, and the corresponding
symbol_table.
Returns
Side-effects on goto_functions, replacing every instanceof in every function with an explicit test. Extra auxiliary variables may be introduced into symbol_table.

Definition at line 218 of file remove_instanceof.cpp.

References remove_instanceoft::lower_instanceof().

Referenced by goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(), symex_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), and remove_instanceof().

◆ remove_instanceof() [2/2]

void remove_instanceof ( goto_modelt goto_model)