10 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H 11 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H 44 const std::vector<bool> &unknown,
46 const typet &type)
const override;
70 return type.
id()==ID_pointer || type.
id()==ID_reference;
74 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H The type of an expression.
literalt convert_rest(const exprt &expr) override
bvt convert_bitvector(const exprt &expr) override
static bool is_ptr(const typet &type)
std::list< postponedt > postponed_listt
const irep_idt & id() const
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
bv_pointerst(const namespacet &_ns, propt &_prop)
postponed_listt postponed_list
void post_process() override
void encode(std::size_t object, bvt &bv)
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Base class for all expressions.
void do_postponed(const postponedt &postponed)
virtual bvt convert_pointer_type(const exprt &expr)
bool convert_address_of_rec(const exprt &expr, bvt &bv)
std::vector< literalt > bvt
void offset_arithmetic(bvt &bv, const mp_integer &x)