CBMC
java_root_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
12 
13 #include <util/irep.h>
14 
15 class struct_exprt;
16 class struct_typet;
17 class symbolt;
18 
19 // adds expected members for a root class,
20 // which is usually java.lang.Object
21 
22 void java_root_class(
23  class symbolt &class_symbol);
24 
25 void java_root_class_init(
26  struct_exprt &jlo,
27  const struct_typet &root_type,
28  const irep_idt &class_identifier);
29 
30 #endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
java_root_class_init
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
Definition: java_root_class.cpp:41
java_root_class
void java_root_class(class symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
Definition: java_root_class.cpp:20
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1818
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:230
symbolt
Symbol table entry.
Definition: symbol.h:27
irep.h