cprover
Loading...
Searching...
No Matches
java_pointer_casts.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Pointer Casts
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_JAVA_BYTECODE_JAVA_POINTER_CASTS_H
13#define CPROVER_JAVA_BYTECODE_JAVA_POINTER_CASTS_H
14
15class exprt;
16class typet;
17class pointer_typet;
18class namespacet;
19
20bool find_superclass_with_type(
21 exprt &ptr,
22 const typet &target_type,
23 const namespacet &ns);
24
25exprt make_clean_pointer_cast(
26 const exprt &ptr,
27 const pointer_typet &target_type,
28 const namespacet &ns);
29
30#endif // CPROVER_JAVA_BYTECODE_JAVA_POINTER_CASTS_H
exprt
Base class for all expressions.
Definition expr.h:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition pointer_expr.h:24
typet
The type of an expression, extends irept.
Definition type.h:29
find_superclass_with_type
bool find_superclass_with_type(exprt &ptr, const typet &target_type, const namespacet &ns)
Definition java_pointer_casts.cpp:32
make_clean_pointer_cast
exprt make_clean_pointer_cast(const exprt &ptr, const pointer_typet &target_type, const namespacet &ns)
Definition java_pointer_casts.cpp:75