cprover
|
JAVA Pointer Casts. More...
#include "java_pointer_casts.h"
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/namespace.h>
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 typet &target_type, const namespacet &ns) |
JAVA Pointer Casts.
Definition in file java_pointer_casts.cpp.
dereference pointer expression
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().
bool find_superclass_with_type | ( | exprt & | ptr, |
const typet & | target_type, | ||
const namespacet & | ns | ||
) |
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().
Definition at line 65 of file java_pointer_casts.cpp.
References irept::id(), exprt::op0(), and exprt::type().
Referenced by make_clean_pointer_cast().
exprt make_clean_pointer_cast | ( | const exprt & | rawptr, |
const typet & | target_type, | ||
const namespacet & | ns | ||
) |
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().