10#ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
11#define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
bool get_array_constraints
std::size_t get_object_width(const pointer_typet &) const
void do_postponed(const postponedt &postponed)
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &)
pointer_logict pointer_logic
NODISCARD bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
postponed_listt postponed_list
std::size_t get_address_width(const pointer_typet &) const
virtual NODISCARD bvt add_addr(const exprt &)
endianness_mapt endianness_map(const typet &, bool little_endian) const override
void finish_eager_conversion() override
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
NODISCARD bvt encode(const mp_integer &object, const pointer_typet &) const
std::list< postponedt > postponed_listt
std::size_t get_offset_width(const pointer_typet &) const
literalt convert_rest(const exprt &) override
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
bvt convert_bitvector(const exprt &) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
bvt object_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to...
bvt offset_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals representing the offset into an object that the p...
virtual bvt convert_pointer_type(const exprt &)
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The type of an expression, extends irept.
std::vector< literalt > bvt
nonstd::optional< T > optionalt
postponedt(bvt _bv, bvt _op, exprt _expr)