cprover
remove_instanceof.h File Reference

Remove Instance-of Operators. More...

#include <util/symbol_table.h>
#include "goto_functions.h"
#include "goto_model.h"
Include dependency graph for remove_instanceof.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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

Detailed Description

Remove Instance-of Operators.

Definition in file remove_instanceof.h.

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 model)