Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
11 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
48 const std::vector<bool> &unknown,
50 const typet &type)
const override;
73 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
bool convert_address_of_rec(const exprt &expr, bvt &bv)
The type of an expression, extends irept.
std::vector< literalt > bvt
postponed_listt postponed_list
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
void do_postponed(const postponedt &postponed)
Base class for all expressions.
exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
virtual bvt convert_pointer_type(const exprt &expr)
std::list< postponedt > postponed_listt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
pointer_logict pointer_logic
void encode(std::size_t object, bvt &bv)
void offset_arithmetic(bvt &bv, const mp_integer &x)
literalt convert_rest(const exprt &expr) override
void post_process() override
virtual void add_addr(const exprt &expr, bvt &bv)