cprover
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/std_expr.h
>
14
15
// adds expected members for a root class,
16
// which is usually java.lang.Object
17
18
void
java_root_class
(
19
class
symbolt
&class_symbol);
20
21
void
java_root_class_init
(
22
struct_exprt
&jlo,
23
const
struct_typet
&root_type,
24
bool
lock,
25
const
irep_idt
&class_identifier);
26
27
#endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
java_root_class
void java_root_class(class symbolt &class_symbol)
Definition:
java_root_class.cpp:28
symbolt
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition:
symbol.h:30
struct_typet
Structure type.
Definition:
std_types.h:297
std_expr.h
API to expression classes.
java_root_class_init
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
Definition:
java_root_class.cpp:62
dstringt
Definition:
dstring.h:21
struct_exprt
struct constructor from list of elements
Definition:
std_expr.h:1815
jbmc
src
java_bytecode
java_root_class.h
Generated by
1.8.14