1/*******************************************************************\
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
10#ifndef CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
11#define CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
18// adds expected members for a root class,
19// which is usually java.lang.Object
29#endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
void java_root_class(class symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
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).