cprover
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 exprtlook_through_casts (const exprt &in)
 
exprt make_clean_pointer_cast (const exprt &rawptr, const 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.

References irept::id(), exprt::op0(), typet::subtype(), and exprt::type().

Referenced by find_superclass_with_type().

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

References clean_deref(), struct_union_typet::components(), namespace_baset::follow(), irept::id(), typet::subtype(), to_struct_type(), and exprt::type().

Referenced by make_clean_pointer_cast().

§ 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 65 of file java_pointer_casts.cpp.

References irept::id(), exprt::op0(), and exprt::type().

Referenced by make_clean_pointer_cast().

§ make_clean_pointer_cast()

exprt make_clean_pointer_cast ( const exprt rawptr,
const typet target_type,
const namespacet ns 
)
parameters: raw pointer
target type namespace
Returns
cleaned up typecast expression

Definition at line 81 of file java_pointer_casts.cpp.

References find_superclass_with_type(), namespace_baset::follow(), irept::id(), look_through_casts(), exprt::op0(), typet::subtype(), and exprt::type().

Referenced by java_bytecode_typecheckt::typecheck_expr().