28 result.reserve(src.size());
30 for(std::size_t i=0; i<src.size(); i++)
32 const size_t mapped_index = map.
map_bit(i);
34 result.push_back(src[mapped_index]);
61 if(expr.
id()==ID_byte_extract_big_endian &&
62 expr.
type().
id()==ID_c_bit_field &&
82 (!index.has_value() || (*index < 0 || *index >= op_bytes)) &&
83 (expr.
op().
id() == ID_member || expr.
op().
id() == ID_index ||
84 expr.
op().
id() == ID_byte_extract_big_endian ||
85 expr.
op().
id() == ID_byte_extract_little_endian))
104 expr.
id() == ID_byte_extract_little_endian ||
105 expr.
id() == ID_byte_extract_big_endian);
106 const bool little_endian = expr.
id() == ID_byte_extract_little_endian;
118 unsigned byte_width=8;
120 if(index.has_value())
122 const mp_integer offset = *index * byte_width;
124 for(std::size_t i=0; i<width; i++)
126 if(offset + i < 0 || offset + i >= op_bv.size())
129 bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
133 std::size_t bytes=op_bv.size()/byte_width;
138 for(std::size_t i=0; i<width; i++)
149 equal_bv.resize(width);
151 for(std::size_t i=0; i<bytes; i++)
155 std::size_t offset=i*byte_width;
157 for(std::size_t j=0; j<width; j++)
158 if(offset+j<op_bv.size())
159 equal_bv[j]=
prop.
lequal(bv[j], op_bv[offset+j]);
174 for(std::size_t i=0; i<bytes; i++)
180 std::size_t offset=i*byte_width;
182 for(std::size_t j=0; j<width; j++)
186 if(offset+j<op_bv.size())
201 bv=
map_bv(result_map, bv);
The type of an expression.
literalt convert(const exprt &expr) override
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
const exprt & root_object() const
exprt flatten_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...
#define CHECK_RETURN(CONDITION)
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 literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual literalt new_variable()=0
Expression classes for byte-level operators.
void util_throw_with_nested(T &&t)
virtual const bvt & convert_bv(const exprt &expr)
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Exceptions that can be raised in bv_conversion.
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
#define PRECONDITION(CONDITION)
split an expression into a base object and a (byte) offset
Map bytes according to the configured endianness.
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
literalt const_literal(bool value)
size_t number_of_bits() const
Base class for all expressions.
virtual bool has_set_to() const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
void make_typecast(const typet &_type)
std::vector< literalt > bvt