cbmc/java__root__class_8h_source.html

/*******************************************************************\


Module:


Author: Daniel Kroening, kroening@kroening.com


\*******************************************************************/


#ifndef CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H

#define CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H


#include <util/irep.h>


class struct_exprt;

class struct_typet;


// adds expected members for a root class,

// which is usually java.lang.Object


void java_root_class(

  class symbolt &class_symbol);


void java_root_class_init(

  struct_exprt &jlo,

  const struct_typet &root_type,

  const irep_idt &class_identifier);


#endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38

struct_exprt
Struct constructor from list of elements.
Definition std_expr.h:1877

struct_typet
Structure type, corresponds to C style structs.
Definition std_types.h:231

symbolt
Symbol table entry.
Definition symbol.h:28

irep.h

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