cprover
Loading...
Searching...
No Matches
java_root_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
15class struct_exprt;
16class struct_typet;
17
18// adds expected members for a root class,
19// which is usually java.lang.Object
20
21void java_root_class(
22 class symbolt &class_symbol);
23
24void java_root_class_init(
25 struct_exprt &jlo,
26 const struct_typet &root_type,
27 const irep_idt &class_identifier);
28
29#endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
struct_exprt
Struct constructor from list of elements.
Definition std_expr.h:1810
struct_typet
Structure type, corresponds to C style structs.
Definition std_types.h:231
symbolt
Symbol table entry.
Definition symbol.h:28
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
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
irep_idt
dstringt irep_idt
Definition verification_result.h:16