cbmc/java__pointer__casts_8h_source.html

/*******************************************************************\


Module: JAVA Pointer Casts


Author: Diffblue Ltd.


\*******************************************************************/


#ifndef CPROVER_JAVA_BYTECODE_JAVA_POINTER_CASTS_H

#define CPROVER_JAVA_BYTECODE_JAVA_POINTER_CASTS_H


class exprt;

class typet;

class pointer_typet;

class namespacet;


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);


#endif // CPROVER_JAVA_BYTECODE_JAVA_POINTER_CASTS_H

exprt
Base class for all expressions.
Definition expr.h:56

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