Go to the documentation of this file.
12 #ifndef CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
13 #define CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
44 const pointert &pointer,
78 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
std::size_t get_null_object() const
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t add_object(const exprt &expr)
Base class for all expressions.
pointer_logict(const namespacet &_ns)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
hash_numbering< exprt, irep_hash > objects
bool is_dynamic_object(const exprt &expr) const
std::size_t invalid_object
std::size_t get_invalid_object() const
pointert(std::size_t _obj, mp_integer _off)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.