12 #ifndef CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H 13 #define CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H 19 #define BV_ADDR_BITS 8 47 const typet &type)
const;
52 const typet &type)
const;
81 const exprt &
object)
const;
86 const exprt &src)
const;
89 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H The type of an expression.
std::size_t get_null_object() const
pointer_typet pointer_type(const typet &subtype)
void get_dynamic_objects(std::vector< std::size_t > &objects) const
hash_numbering< exprt, irep_hash > objectst
std::size_t get_invalid_object() const
pointert(std::size_t _obj, mp_integer _off)
bool is_dynamic_object(const exprt &expr) const
exprt pointer_expr(const pointert &pointer, const typet &type) const
pointer_logict(const namespacet &_ns)
Base class for all expressions.
std::size_t add_object(const exprt &expr)
exprt object_rec(const mp_integer &offset, const typet &pointer_type, const exprt &src) const
std::size_t invalid_object