Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
11 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
74 const typet &type)
const override;
103 :
bv(std::move(_bv)),
op(std::move(_op)),
expr(std::move(_expr))
125 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
138 return bvt(bv.begin(), bv.begin() + offset_width);
149 result.reserve(offset.size() +
object.size());
150 result.insert(result.end(), offset.begin(), offset.end());
151 result.insert(result.end(),
object.begin(),
object.end());
157 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
postponedt(bvt _bv, bvt _op, exprt _expr)
std::size_t operator()(const typet &type) const override
exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const override
The type of an expression, extends irept.
std::vector< literalt > bvt
std::size_t boolbv_width(const typet &type) const override
postponed_listt postponed_list
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...
void do_postponed(const postponedt &postponed)
Base class for all expressions.
virtual bvt convert_pointer_type(const exprt &expr)
std::list< postponedt > postponed_listt
std::size_t get_address_width(const pointer_typet &type) const
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...
#define PRECONDITION(CONDITION)
std::size_t get_object_width(const pointer_typet &type) const
pointer_logict pointer_logic
NODISCARD bvt offset_arithmetic(const pointer_typet &type, const bvt &bv, const mp_integer &x)
nonstd::optional< T > optionalt
std::size_t get_offset_width(const pointer_typet &type) const
virtual NODISCARD bvt add_addr(const exprt &expr)
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &expr)
bv_pointers_widtht bv_pointers_width
Maps a big-endian offset to a little-endian offset.
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
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...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
bool get_array_constraints
literalt convert_rest(const exprt &expr) override
void post_process() override
message_handlert & message_handler
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
bv_pointers_widtht(const namespacet &_ns)
NODISCARD bvt encode(std::size_t object, const pointer_typet &type) const