27 for(std::size_t i=0; i<src.size(); i++)
29 size_t mapped_index=map.
map_bit(i);
30 assert(mapped_index<src.size());
31 result[i]=src[mapped_index];
40 throw "byte_extract takes two operands";
54 if(expr.
id()==ID_byte_extract_big_endian &&
55 expr.
type().
id()==ID_c_bit_field &&
75 if(expr.
id()==ID_byte_extract_little_endian)
77 else if(expr.
id()==ID_byte_extract_big_endian)
96 unsigned byte_width=8;
102 throw "byte_extract flatting with negative offset: "+expr.
pretty();
108 for(std::size_t i=0; i<width; i++)
110 if(offset<0 || offset_i+i>=op_bv.size())
113 bv[i]=op_bv[offset_i+i];
117 std::size_t bytes=op_bv.size()/byte_width;
122 for(std::size_t i=0; i<width; i++)
128 equality.
lhs()=offset;
133 equal_bv.resize(width);
135 for(std::size_t i=0; i<bytes; i++)
139 std::size_t offset=i*byte_width;
141 for(std::size_t j=0; j<width; j++)
142 if(offset+j<op_bv.size())
143 equal_bv[j]=
prop.
lequal(bv[j], op_bv[offset+j]);
154 equality.
lhs()=offset;
158 for(std::size_t i=0; i<bytes; i++)
164 std::size_t offset=i*byte_width;
166 for(std::size_t j=0; j<width; j++)
170 if(offset+j<op_bv.size())
185 bv=
map_bv(result_map, bv);
The type of an expression.
Maps a big-endian offset to a little-endian offset.
virtual literalt convert(const exprt &expr) override
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
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...
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.
virtual const bvt & convert_bv(const exprt &expr)
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
virtual literalt lequal(literalt a, literalt b)=0
unsigned integer2unsigned(const mp_integer &n)
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
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::vector< literalt > bvt