Go to the documentation of this file.
27 result.reserve(src.size());
29 for(std::size_t i=0; i<src.size(); i++)
31 const size_t mapped_index = map.
map_bit(i);
33 result.push_back(src[mapped_index]);
53 if(expr.
id()==ID_byte_extract_big_endian &&
54 expr.
type().
id()==ID_c_bit_field &&
72 auto index = numeric_cast<mp_integer>(expr.
offset());
75 (!index.has_value() || !op_bytes_opt.has_value() ||
76 *index < 0 || *index >= *op_bytes_opt) &&
77 (expr.
op().
id() == ID_member ||
78 expr.
op().
id() == ID_index ||
79 expr.
op().
id() == ID_byte_extract_big_endian ||
80 expr.
op().
id() == ID_byte_extract_little_endian))
100 expr.
id() == ID_byte_extract_little_endian ||
101 expr.
id() == ID_byte_extract_big_endian);
102 const bool little_endian = expr.
id() == ID_byte_extract_little_endian;
114 unsigned byte_width=8;
116 if(index.has_value())
118 const mp_integer offset = *index * byte_width;
120 for(std::size_t i=0; i<width; i++)
122 if(offset + i < 0 || offset + i >= op_bv.size())
125 bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
129 std::size_t bytes=op_bv.size()/byte_width;
134 for(std::size_t i=0; i<width; i++)
143 equal_bv.resize(width);
145 for(std::size_t i=0; i<bytes; i++)
147 std::size_t offset=i*byte_width;
149 for(std::size_t j=0; j<width; j++)
150 if(offset+j<op_bv.size())
151 equal_bv[j]=
prop.
lequal(bv[j], op_bv[offset+j]);
165 for(std::size_t i=0; i<bytes; i++)
170 std::size_t offset=i*byte_width;
172 for(std::size_t j=0; j<width; j++)
176 if(offset+j<op_bv.size())
191 bv=
map_bv(result_map, bv);
static exprt conditional_cast(const exprt &expr, const typet &type)
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
bool is_unbounded_array(const typet &type) const override
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< literalt > bvt
Map bytes according to the configured endianness.
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
virtual literalt new_variable()=0
Base class for all expressions.
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
typet & type()
Return the type of the expression.
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Expression classes for byte-level operators.
boolbv_widtht boolbv_width
size_t number_of_bits() const
void conversion_failed(const exprt &expr, bvt &bv)
virtual literalt limplies(literalt a, literalt b)=0
#define PRECONDITION(CONDITION)
size_t map_bit(size_t bit) const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
literalt const_literal(bool value)
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
const exprt & root_object() const
void set_width(std::size_t width)
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Deprecated expression utility functions.
virtual literalt lequal(literalt a, literalt b)=0
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual bool has_set_to() const
API to expression classes.
virtual literalt lselect(literalt a, literalt b, literalt c)=0