Loading...

Searching...

No Matches

java_root_class.cpp File Reference

#include "java_root_class.h"
#include <goto-programs/class_identifier.h>
#include <util/arith_tools.h>
#include <util/symbol.h>

+ Include dependency graph for java_root_class.cpp:

Functions

Create components to an object of the root class (usually java.lang.Object) Specifically, we add a new component, '@class_identifier'.

Adds members for an object of the root class (usually java.lang.Object).

Function Documentation

void java_root_class ( symbolt & class_symbol )

Create components to an object of the root class (usually java.lang.Object) Specifically, we add a new component, '@class_identifier'.

This used primary to replace an expression like 'e instanceof A' with 'e.@class_identifier == "A"'

Definition at line 20 of file java_root_class.cpp.

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).

Parameters: [out] jlo object to initialize

root_type type of the root class

class_identifier class identifier field, generally begins with "java::" prefix.

Definition at line 41 of file java_root_class.cpp.