java_pointer_casts.cpp File Reference

JAVA Pointer Casts. More...

#include "java_pointer_casts.h"
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/namespace.h>

Include dependency graph for java_pointer_casts.cpp:

Go to the source code of this file.

Functions
static exprt	clean_deref (const exprt &ptr)
	dereference pointer expression More...
bool	find_superclass_with_type (exprt &ptr, const typet &target_type, const namespacet &ns)
static const exprt &	look_through_casts (const exprt &in)
exprt	make_clean_pointer_cast (const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)

Detailed Description

JAVA Pointer Casts.

Definition in file java_pointer_casts.cpp.

Function Documentation

clean_deref()

static exprt clean_deref ( const exprt &  ptr )

static

dereference pointer expression

Returns

dereferenced pointer

Definition at line 20 of file java_pointer_casts.cpp.

find_superclass_with_type()

bool find_superclass_with_type	(	exprt &	ptr,
		const typet &	target_type,
		const namespacet &	ns
	)

parameters: pointer

target type to search

Returns

true iff a super class with target type is found

Definition at line 30 of file java_pointer_casts.cpp.

look_through_casts()

static const exprt& look_through_casts ( const exprt &  in )

static

parameters: input expression

Returns

recursively search target of typecast

Definition at line 69 of file java_pointer_casts.cpp.

make_clean_pointer_cast()

exprt make_clean_pointer_cast	(	const exprt &	rawptr,
		const pointer_typet &	target_type,
		const namespacet &	ns
	)

parameters: raw pointer

target type namespace

Returns

cleaned up typecast expression

Definition at line 85 of file java_pointer_casts.cpp.