cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
remove_instanceof.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Remove Instance-of Operators
4
5
Author: Chris Smowton, chris.smowton@diffblue.com
6
7
\*******************************************************************/
8
78
79
#ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
80
#define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
81
82
#include <
goto-programs/goto_functions.h
>
83
84
class
class_hierarchyt
;
85
class
goto_modelt
;
86
class
message_handlert
;
87
class
symbol_table_baset
;
88
89
void
remove_instanceof
(
90
const
irep_idt
&function_identifier,
91
goto_programt::targett
target,
92
goto_programt
&goto_program,
93
symbol_table_baset
&symbol_table,
94
const
class_hierarchyt
&class_hierarchy,
95
message_handlert
&);
96
97
void
remove_instanceof
(
98
const
irep_idt
&function_identifier,
99
goto_functionst::goto_functiont
&function,
100
symbol_table_baset
&symbol_table,
101
const
class_hierarchyt
&class_hierarchy,
102
message_handlert
&);
103
104
void
remove_instanceof
(
105
goto_functionst
&goto_functions,
106
symbol_table_baset
&symbol_table,
107
const
class_hierarchyt
&class_hierarchy,
108
message_handlert
&);
109
110
void
remove_instanceof
(
111
goto_modelt
&model,
112
const
class_hierarchyt
&class_hierarchy,
113
message_handlert
&);
114
115
#endif
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition
class_hierarchy.h:41
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition
goto_functions.h:27
goto_modelt
Definition
goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
goto_programt::targett
instructionst::iterator targett
Definition
goto_program.h:613
message_handlert
Definition
message.h:27
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
goto_functions.h
Goto Programs with Functions.
remove_instanceof
void remove_instanceof(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Definition
remove_instanceof.cpp:306
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
jbmc
src
java_bytecode
remove_instanceof.h
Generated by
1.17.0