40 for(
const auto &comp : components)
44 if(!element_width.has_value() || *element_width <= max_width)
47 max_width = *element_width;
48 max_comp_type = comp.type();
49 max_comp_name = comp.get_name();
55 return std::make_pair(
60 const exprt &bitvector_expr,
61 const typet &target_type,
74 std::size_t lower_bound,
75 std::size_t upper_bound)
78 result.
lb = lower_bound;
79 result.
ub = upper_bound;
87 if(result.
ub < result.
lb)
100 const exprt &bitvector_expr,
108 operands.reserve(components.size());
110 for(
const auto &comp : components)
113 std::size_t component_bits;
114 if(component_bits_opt.has_value())
115 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
120 if(component_bits == 0)
137 if(component_bits_opt.has_value())
147 const exprt &bitvector_expr,
155 if(components.empty())
160 std::size_t component_bits;
161 if(widest_member.has_value())
162 component_bits = numeric_cast_v<std::size_t>(widest_member->second);
166 if(component_bits == 0)
173 const auto bounds =
map_bounds(endianness_map, 0, component_bits - 1);
175 const irep_idt &component_name = widest_member.has_value()
176 ? widest_member->first.get_name()
177 : components.front().get_name();
178 const typet &component_type = widest_member.has_value()
179 ? widest_member->first.type()
180 : components.front().type();
194 const exprt &bitvector_expr,
199 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
202 const std::size_t total_bits =
204 if(!num_elements.has_value())
206 if(!subtype_bits.has_value() || *subtype_bits == 0)
207 num_elements = total_bits;
209 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
212 !num_elements.has_value() || !subtype_bits.has_value() ||
213 *subtype_bits * *num_elements == total_bits,
214 "subtype width times array size should be total bitvector width");
217 operands.reserve(*num_elements);
218 for(std::size_t i = 0; i < *num_elements; ++i)
220 if(subtype_bits.has_value())
222 const std::size_t subtype_bits_int =
223 numeric_cast_v<std::size_t>(*subtype_bits);
225 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
229 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
241 return array_exprt{std::move(operands), array_type};
247 const exprt &bitvector_expr,
252 const std::size_t num_elements =
253 numeric_cast_v<std::size_t>(vector_type.
size());
256 !subtype_bits.has_value() ||
257 *subtype_bits * num_elements ==
259 "subtype width times vector size should be total bitvector width");
262 operands.reserve(num_elements);
263 for(std::size_t i = 0; i < num_elements; ++i)
265 if(subtype_bits.has_value())
267 const std::size_t subtype_bits_int =
268 numeric_cast_v<std::size_t>(*subtype_bits);
270 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
274 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
292 const exprt &bitvector_expr,
297 const std::size_t total_bits =
300 std::size_t subtype_bits;
301 if(subtype_bits_opt.has_value())
303 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
305 subtype_bits * 2 == total_bits,
306 "subtype width should be half of the total bitvector width");
309 subtype_bits = total_bits / 2;
311 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
312 const auto bounds_imag =
313 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
345 const exprt &bitvector_expr,
346 const typet &target_type,
354 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
355 target_type.
id() == ID_string)
364 if(target_type.
id() == ID_struct)
369 else if(target_type.
id() == ID_struct_tag)
376 result.
type() = target_type;
377 return std::move(result);
379 else if(target_type.
id() == ID_union)
382 bitvector_expr,
to_union_type(target_type), endianness_map, ns);
384 else if(target_type.
id() == ID_union_tag)
391 result.
type() = target_type;
392 return std::move(result);
394 else if(target_type.
id() == ID_array)
397 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
399 else if(target_type.
id() == ID_vector)
404 else if(target_type.
id() == ID_complex)
412 false,
"bv_to_expr does not yet support ", target_type.
id_string());
422 bool unpack_byte_array =
false);
432 std::size_t lower_bound,
433 std::size_t upper_bound,
438 if(src.
id() == ID_array)
442 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
443 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
447 bytes.reserve(upper_bound - lower_bound);
448 for(std::size_t i = lower_bound; i < upper_bound; ++i)
478 const std::size_t el_bytes =
479 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
481 if(!src_size.has_value() && !max_bytes.has_value())
485 static std::size_t array_comprehension_index_counter = 0;
486 ++array_comprehension_index_counter;
488 "$array_comprehension_index_a_v" +
501 exprt body = sub_operands.front();
503 array_comprehension_index,
504 from_integer(el_bytes, array_comprehension_index.type())};
505 for(std::size_t i = 1; i < el_bytes; ++i)
515 if(src.
type().
id() == ID_vector)
527 std::move(array_comprehension_index),
541 if(element_bits > 0 && element_bits % 8 == 0)
543 if(!num_elements.has_value())
546 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
549 if(offset_bytes.has_value())
552 first_element = *offset_bytes / el_bytes;
554 byte_operands.resize(
555 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
564 num_elements = *max_bytes;
568 for(
mp_integer i = first_element; i < *num_elements; ++i)
573 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
576 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
577 element = src_simp.
operands()[index_int];
586 exprt sub =
unpack_rec(element, little_endian, {}, max_bytes, ns,
true);
589 byte_operands.insert(
590 byte_operands.end(), sub_operands.begin(), sub_operands.end());
593 const std::size_t size = byte_operands.size();
595 std::move(byte_operands),
611 std::size_t total_bits,
622 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns,
true);
626 std::make_move_iterator(sub.
operands().begin()),
627 std::make_move_iterator(sub.
operands().end()));
655 for(
auto it = components.begin(); it != components.end(); ++it)
657 const auto &comp = *it;
666 component_bits.has_value() ||
667 (std::next(it) == components.end() && !bit_fields.has_value()),
668 "members of non-constant width should come last in a struct");
671 if(src.
id() == ID_struct)
677 if(bit_fields.has_value())
680 std::move(bit_fields->first),
690 if(offset_bytes.has_value())
695 if(*offset_in_member < 0)
696 offset_in_member.reset();
699 if(max_bytes.has_value())
702 if(*max_bytes_left < 0)
709 (component_bits.has_value() && *component_bits % 8 != 0))
711 if(!bit_fields.has_value())
714 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
715 bit_fields->first.insert(
716 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
718 bit_fields->second += bits_int;
726 !bit_fields.has_value(),
727 "all preceding members should have been processed");
730 member, little_endian, offset_in_member, max_bytes_left, ns,
true);
732 byte_operands.insert(
734 std::make_move_iterator(sub.
operands().begin()),
735 std::make_move_iterator(sub.
operands().end()));
737 if(component_bits.has_value())
741 if(bit_fields.has_value())
743 std::move(bit_fields->first),
751 const std::size_t size = byte_operands.size();
787 byte_operands.insert(
789 std::make_move_iterator(sub_imag.
operands().begin()),
790 std::make_move_iterator(sub_imag.
operands().end()));
792 const std::size_t size = byte_operands.
size();
814 bool unpack_byte_array)
816 if(src.
type().
id()==ID_array)
824 if(!unpack_byte_array && *element_bits == 8)
827 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
837 else if(src.
type().
id() == ID_vector)
845 if(!unpack_byte_array && *element_bits == 8)
850 numeric_cast_v<mp_integer>(vector_type.
size()),
857 else if(src.
type().
id() == ID_complex)
861 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
863 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
865 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
874 for(
const auto &comp : components)
878 if(!element_width.has_value() || *element_width <= max_width)
881 max_width = *element_width;
882 max_comp_type = comp.type();
883 max_comp_name = comp.get_name();
890 member, little_endian, offset_bytes, max_bytes, ns,
true);
893 else if(src.
type().
id() == ID_pointer)
903 else if(src.
id() == ID_string_constant)
913 else if(src.
id() == ID_constant && src.
type().
id() == ID_string)
923 else if(src.
type().
id()!=ID_empty)
928 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
936 src,
bv_typet{numeric_cast_v<std::size_t>(bits)}),
945 byte_operands.push_back(extractbits);
947 byte_operands.insert(byte_operands.begin(), extractbits);
950 const std::size_t size = byte_operands.
size();
952 std::move(byte_operands),
977 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
982 real.
type() = subtype;
988 imag.
type() = subtype;
1047 src.
id() == ID_byte_extract_little_endian ||
1048 src.
id() == ID_byte_extract_big_endian);
1049 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
1053 if(upper_bound_opt.has_value())
1057 upper_bound_opt.value(),
1059 src.
offset(), upper_bound_opt.value().
type())),
1062 else if(src.
type().
id() == ID_empty)
1065 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
1066 const auto upper_bound_int_opt =
1067 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
1071 src.
op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1073 if(src.
type().
id()==ID_array)
1082 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1084 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
1085 if(!num_elements.has_value() && unpacked.
op().
id() == ID_array)
1086 num_elements = unpacked.
op().
operands().size();
1088 if(num_elements.has_value())
1091 operands.reserve(*num_elements);
1092 for(std::size_t i = 0; i < *num_elements; ++i)
1099 tmp.
type() = subtype;
1100 tmp.
offset() = new_offset;
1111 static std::size_t array_comprehension_index_counter = 0;
1112 ++array_comprehension_index_counter;
1114 "$array_comprehension_index_a" +
1123 *element_bits / 8, array_comprehension_index.type())},
1127 body.
type() = subtype;
1128 body.
offset() = std::move(new_offset);
1136 else if(src.
type().
id() == ID_vector)
1145 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1147 const std::size_t num_elements =
1148 numeric_cast_v<std::size_t>(vector_type.
size());
1151 operands.reserve(num_elements);
1152 for(std::size_t i = 0; i < num_elements; ++i)
1159 tmp.
type() = subtype;
1168 else if(src.
type().
id() == ID_complex)
1171 if(result.has_value())
1172 return std::move(*result);
1176 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1184 for(
const auto &comp : components)
1190 !component_bits.has_value() || *component_bits == 0 ||
1191 *component_bits % 8 != 0)
1197 auto member_offset_opt =
1200 if(!member_offset_opt.has_value())
1209 member_offset_opt.value(), unpacked.
offset().
type()));
1212 tmp.
type()=comp.type();
1221 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1227 if(widest_member.has_value())
1230 tmp.
type() = widest_member->first.type();
1233 widest_member->first.get_name(),
1239 const exprt &root=unpacked.
op();
1243 if(root.
type().
id() == ID_vector)
1251 subtype_bits.has_value() && *subtype_bits == 8,
1252 "offset bits are byte aligned");
1255 if(!size_bits.has_value())
1260 op0_bits.has_value(),
1261 "the extracted width or the source width must be known");
1262 size_bits = op0_bits;
1266 (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1269 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_elements);
1271 op.reserve(width_bytes);
1273 for(std::size_t i=0; i<width_bytes; i++)
1276 std::size_t offset_int=
1277 little_endian?(width_bytes-i-1):i;
1284 offset_i.is_constant() &&
1285 (root.
id() == ID_array || root.
id() == ID_vector) &&
1287 index < root.
operands().size() && index >= 0)
1290 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1315 const exprt &value_as_byte_array,
1330 const typet &subtype,
1331 const exprt &value_as_byte_array,
1332 const exprt &non_const_update_bound,
1337 static std::size_t array_comprehension_index_counter = 0;
1338 ++array_comprehension_index_counter;
1340 "$array_comprehension_index_u_a_v" +
1346 array_comprehension_index, src.
offset().
type()),
1351 array_comprehension_index, non_const_update_bound.
type()),
1354 src.
offset(), non_const_update_bound.
type()),
1355 non_const_update_bound}};
1358 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1362 value_as_byte_array,
1365 src.
offset(), array_comprehension_index.
type())}},
1370 std::move(array_comprehension_body),
1386 const typet &subtype,
1394 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1404 if(e.id() == ID_index)
1407 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1412 if(non_const_update_bound.has_value())
1418 *non_const_update_bound},
1426 if(result.
id() != ID_with)
1427 result =
with_exprt{result, where, update_value};
1452 const typet &subtype,
1453 const exprt &subtype_size,
1454 const exprt &value_as_byte_array,
1455 const exprt &non_const_update_bound,
1456 const exprt &initial_bytes,
1457 const exprt &first_index,
1458 const exprt &first_update_value,
1461 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1462 ? ID_byte_extract_little_endian
1463 : ID_byte_extract_big_endian;
1467 static std::size_t array_comprehension_index_counter = 0;
1468 ++array_comprehension_index_counter;
1470 "$array_comprehension_index_u_a_v_u" +
1482 array_comprehension_index, first_index.
type()),
1491 array_comprehension_index, first_index.
type()),
1495 extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1504 non_const_update_bound, subtype_size.
type()),
1516 non_const_update_bound, initial_bytes.
type()),
1524 array_comprehension_index, last_index.type()),
1537 value_as_byte_array,
1539 last_index, subtype_size.
type()),
1545 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1549 array_comprehension_index, first_index.
type()),
1553 array_comprehension_index, last_index.type()),
1555 std::move(last_update_value),
1556 std::move(update_value)}}};
1560 std::move(array_comprehension_body),
1577 const typet &subtype,
1578 const exprt &value_as_byte_array,
1582 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1583 ? ID_byte_extract_little_endian
1584 : ID_byte_extract_big_endian;
1593 subtype_size_opt.value(), src.
offset().
type()),
1608 if(non_const_update_bound.has_value())
1611 *non_const_update_bound, subtype_size.
type());
1616 value_as_byte_array.
id() == ID_array,
1617 "value should be an array expression if the update bound is constant");
1635 value_as_byte_array,
1640 if(value_as_byte_array.
id() != ID_array)
1646 value_as_byte_array,
1647 *non_const_update_bound,
1659 std::size_t step_size = 1;
1666 std::size_t offset = 0;
1670 with_exprt result{src.
op(), first_index, first_update_value};
1673 for(; offset + step_size <= value_as_byte_array.
operands().size();
1674 offset += step_size, ++i)
1691 value_as_byte_array,
1692 std::move(offset_expr),
1700 if(offset < value_as_byte_array.
operands().size())
1702 const std::size_t tail_size =
1703 value_as_byte_array.
operands().size() - offset;
1715 value_as_byte_array,
1737 const typet &subtype,
1738 const exprt &value_as_byte_array,
1742 const bool is_array = src.
type().
id() == ID_array;
1754 !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1755 non_const_update_bound.has_value() || value_as_byte_array.
id() != ID_array)
1758 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1761 std::size_t num_elements =
1767 elements.reserve(num_elements);
1771 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1775 for(; i < num_elements &&
1777 (offset_bytes + value_as_byte_array.operands().size()) * 8;
1780 mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1781 mp_integer update_elements = *subtype_bits / 8;
1782 exprt::operandst::const_iterator first =
1783 value_as_byte_array.operands().begin();
1784 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1785 if(update_offset < 0)
1788 value_as_byte_array.operands().size() > -update_offset,
1789 "indices past the update should be handled above");
1790 first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1794 update_elements -= update_offset;
1796 update_elements > 0,
1797 "indices before the update should be handled above");
1800 if(std::distance(first, end) > update_elements)
1801 end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1803 const std::size_t update_size = update_values.size();
1808 from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1810 std::move(update_values),
1816 for(; i < num_elements; ++i)
1817 elements.push_back(
index_exprt{src.op(), from_integer(i, index_type())});
1839 const exprt &value_as_byte_array,
1843 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1844 ? ID_byte_extract_little_endian
1845 : ID_byte_extract_big_endian;
1848 elements.reserve(struct_type.
components().size());
1851 for(
const auto &comp : struct_type.
components())
1863 auto offset_bytes = numeric_cast<mp_integer>(offset);
1870 offset_bytes.has_value() &&
1871 (*offset_bytes * 8 >= *element_width ||
1872 (value_as_byte_array.
id() == ID_array && *offset_bytes < 0 &&
1873 -*offset_bytes >= value_as_byte_array.
operands().size())))
1875 elements.push_back(std::move(member));
1879 else if(!offset_bytes.has_value())
1902 bu, value_as_byte_array, non_const_update_bound, ns),
1912 mp_integer update_elements = (*element_width + 7) / 8;
1913 std::size_t first = 0;
1914 if(*offset_bytes < 0)
1918 value_as_byte_array.
id() != ID_array ||
1919 value_as_byte_array.
operands().size() > -*offset_bytes,
1920 "members past the update should be handled above");
1921 first = numeric_cast_v<std::size_t>(-*offset_bytes);
1925 update_elements -= *offset_bytes;
1927 update_elements > 0,
1928 "members before the update should be handled above");
1934 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1935 if(value_as_byte_array.
id() == ID_array)
1936 end = std::min(end, value_as_byte_array.
operands().size());
1939 const std::size_t update_size = update_values.size();
1948 if(non_const_update_bound.has_value())
1956 *non_const_update_bound,
1968 remaining_update_bytes};
1970 member_update_bound = std::move(update_size_expr);
1975 const std::size_t shift =
1977 const std::size_t element_bits_int =
1978 numeric_cast_v<std::size_t>(*element_width);
1980 const bool little_endian = src.
id() == ID_byte_update_little_endian;
1986 bv_typet{shift + element_bits_int}};
1995 exprt updated_element =
1999 elements.push_back(updated_element);
2004 element_bits_int - 1 + (little_endian ? shift : 0),
2005 (little_endian ? shift : 0),
2028 const exprt &value_as_byte_array,
2035 widest_member.has_value(),
2036 "lower_byte_update of union of unknown size is not supported");
2040 src.
op(), widest_member->first.get_name(), widest_member->first.
type()});
2041 bu.
type() = widest_member->first.type();
2044 widest_member->first.get_name(),
2059 const exprt &value_as_byte_array,
2063 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
2066 if(src.
type().
id() == ID_vector)
2076 if(*element_width == 8)
2078 if(value_as_byte_array.
id() != ID_array)
2081 non_const_update_bound.has_value(),
2082 "constant update bound should yield an array expression");
2084 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2091 non_const_update_bound,
2096 src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2098 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
2103 value_as_byte_array,
2104 non_const_update_bound,
2109 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
2114 value_as_byte_array,
2115 non_const_update_bound,
2122 src.
type().
id() == ID_c_enum || src.
type().
id() == ID_c_enum_tag)
2127 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2128 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2131 if(value_as_byte_array.
id() == ID_array)
2132 update_bytes = value_as_byte_array.
operands();
2139 if(non_const_update_bound.has_value())
2143 src.
id() == ID_byte_update_little_endian,
2149 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2155 *non_const_update_bound},
2161 const std::size_t update_size = update_bytes.size();
2162 const std::size_t width = std::max(type_bits, update_size * 8);
2164 const bool is_little_endian = src.
id() == ID_byte_update_little_endian;
2168 if(is_little_endian)
2180 offset_times_eight, ID_ge,
from_integer(0, offset_type)};
2182 if_exprt mask_shifted{offset_ge_zero,
2185 if(!is_little_endian)
2186 mask_shifted.true_case().
swap(mask_shifted.false_case());
2191 if(width > type_bits)
2198 if(!is_little_endian)
2207 if(is_little_endian)
2208 std::reverse(value.operands().begin(), value.operands().end());
2210 exprt zero_extended;
2211 if(width > update_size * 8)
2218 if(!is_little_endian)
2224 zero_extended = value;
2227 if_exprt value_shifted{offset_ge_zero,
2228 shl_exprt{zero_extended, offset_times_eight},
2229 lshr_exprt{zero_extended, offset_times_eight}};
2230 if(!is_little_endian)
2231 value_shifted.true_case().
swap(value_shifted.false_case());
2234 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2236 if(!is_little_endian && width > type_bits)
2241 bitor_expr, width - 1, width - type_bits,
bv_typet{type_bits}},
2252 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2259 src.
id() == ID_byte_update_little_endian ||
2260 src.
id() == ID_byte_update_big_endian,
2261 "byte update expression should either be little or big endian");
2280 simplify(update_size_expr_opt.value(), ns);
2282 if(!update_size_expr_opt.value().is_constant())
2283 non_const_update_bound = *update_size_expr_opt;
2285 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2286 ? ID_byte_extract_little_endian
2287 : ID_byte_extract_big_endian;
2304 if(src.
id()==ID_byte_update_little_endian ||
2305 src.
id()==ID_byte_update_big_endian ||
2306 src.
id()==ID_byte_extract_little_endian ||
2307 src.
id()==ID_byte_extract_big_endian)
2327 if(src.
id()==ID_byte_update_little_endian ||
2328 src.
id()==ID_byte_update_big_endian)
2330 else if(src.
id()==ID_byte_extract_little_endian ||
2331 src.
id()==ID_byte_extract_big_endian)