CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/remove_instanceof.h Source File

CBMC

Loading...

Searching...

No Matches

remove_instanceof.h

Go to the documentation of this file.

1/*******************************************************************\

2

3Module: Remove Instance-of Operators

4

5Author: 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

84class class_hierarchyt;

85class goto_modelt;

86class message_handlert;

87class symbol_table_baset;

88

89void 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

97void 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

104void remove_instanceof(

105 goto_functionst &goto_functions,

106 symbol_table_baset &symbol_table,

107 const class_hierarchyt &class_hierarchy,

108 message_handlert &);

109

110void 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

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

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

Definition goto_model.h:27

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