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:

Go to the source code of this file.

Functions
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'. More...
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). More...

Function Documentation

java_root_class()

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"'

Parameters

class_symbol

class symbol

Definition at line 20 of file java_root_class.cpp.

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

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.