cprover
|
JAVA Pointer Casts. More...
Go to the source code of this file.
Functions | |
bool | find_superclass_with_type (exprt &ptr, const typet &target_type, const namespacet &ns) |
exprt | make_clean_pointer_cast (const exprt &ptr, const pointer_typet &target_type, const namespacet &ns) |
JAVA Pointer Casts.
Definition in file java_pointer_casts.h.
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().
exprt make_clean_pointer_cast | ( | const exprt & | rawptr, |
const pointer_typet & | target_type, | ||
const namespacet & | ns | ||
) |
Definition at line 85 of file java_pointer_casts.cpp.
References find_superclass_with_type(), namespace_baset::follow(), irept::id(), look_through_casts(), exprt::op0(), PRECONDITION, typet::subtype(), and exprt::type().
Referenced by java_simple_method_stubst::create_method_stub_at(), and java_bytecode_typecheckt::typecheck_expr().