26 const exprt &bitvector_expr,
27 const typet &target_type,
40 std::size_t lower_bound,
41 std::size_t upper_bound)
44 result.
lb = lower_bound;
45 result.
ub = upper_bound;
53 if(result.
ub < result.
lb)
66 const exprt &bitvector_expr,
74 operands.reserve(components.size());
76 for(
const auto &comp : components)
79 std::size_t component_bits;
80 if(component_bits_opt.has_value())
81 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
86 if(component_bits == 0)
103 if(component_bits_opt.has_value())
113 const exprt &bitvector_expr,
121 if(components.empty())
126 std::size_t component_bits;
127 if(widest_member.has_value())
128 component_bits = numeric_cast_v<std::size_t>(widest_member->second);
132 if(component_bits == 0)
139 const auto bounds =
map_bounds(endianness_map, 0, component_bits - 1);
141 const irep_idt &component_name = widest_member.has_value()
142 ? widest_member->first.get_name()
143 : components.front().get_name();
144 const typet &component_type = widest_member.has_value()
145 ? widest_member->first.type()
146 : components.front().type();
160 const exprt &bitvector_expr,
165 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
168 const std::size_t total_bits =
170 if(!num_elements.has_value())
172 if(!subtype_bits.has_value() || *subtype_bits == 0)
173 num_elements = total_bits;
175 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
178 !num_elements.has_value() || !subtype_bits.has_value() ||
179 *subtype_bits * *num_elements == total_bits,
180 "subtype width times array size should be total bitvector width");
183 operands.reserve(*num_elements);
184 for(std::size_t i = 0; i < *num_elements; ++i)
186 if(subtype_bits.has_value())
188 const std::size_t subtype_bits_int =
189 numeric_cast_v<std::size_t>(*subtype_bits);
191 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
195 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
207 return array_exprt{std::move(operands), array_type};
213 const exprt &bitvector_expr,
218 const std::size_t num_elements =
219 numeric_cast_v<std::size_t>(vector_type.
size());
222 !subtype_bits.has_value() ||
223 *subtype_bits * num_elements ==
225 "subtype width times vector size should be total bitvector width");
228 operands.reserve(num_elements);
229 for(std::size_t i = 0; i < num_elements; ++i)
231 if(subtype_bits.has_value())
233 const std::size_t subtype_bits_int =
234 numeric_cast_v<std::size_t>(*subtype_bits);
236 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
240 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
258 const exprt &bitvector_expr,
263 const std::size_t total_bits =
266 std::size_t subtype_bits;
267 if(subtype_bits_opt.has_value())
269 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
271 subtype_bits * 2 == total_bits,
272 "subtype width should be half of the total bitvector width");
275 subtype_bits = total_bits / 2;
277 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
278 const auto bounds_imag =
279 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
311 const exprt &bitvector_expr,
312 const typet &target_type,
320 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
321 target_type.
id() == ID_string)
330 if(target_type.
id() == ID_struct)
335 else if(target_type.
id() == ID_struct_tag)
342 result.
type() = target_type;
343 return std::move(result);
345 else if(target_type.
id() == ID_union)
348 bitvector_expr,
to_union_type(target_type), endianness_map, ns);
350 else if(target_type.
id() == ID_union_tag)
357 result.
type() = target_type;
358 return std::move(result);
360 else if(target_type.
id() == ID_array)
363 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
365 else if(target_type.
id() == ID_vector)
370 else if(target_type.
id() == ID_complex)
378 false,
"bv_to_expr does not yet support ", target_type.
id_string());
388 bool unpack_byte_array =
false);
398 std::size_t lower_bound,
399 std::size_t upper_bound,
404 if(src.
id() == ID_array)
408 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
409 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
413 bytes.reserve(upper_bound - lower_bound);
414 for(std::size_t i = lower_bound; i < upper_bound; ++i)
444 const std::size_t el_bytes =
445 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
447 if(!src_size.has_value() && !max_bytes.has_value())
451 static std::size_t array_comprehension_index_counter = 0;
452 ++array_comprehension_index_counter;
454 "$array_comprehension_index_a_v" +
467 exprt body = sub_operands.front();
469 array_comprehension_index,
470 from_integer(el_bytes, array_comprehension_index.type())};
471 for(std::size_t i = 1; i < el_bytes; ++i)
479 const exprt array_vector_size = src.
type().
id() == ID_vector
484 std::move(array_comprehension_index),
498 if(element_bits > 0 && element_bits % 8 == 0)
500 if(!num_elements.has_value())
503 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
506 if(offset_bytes.has_value())
509 first_element = *offset_bytes / el_bytes;
511 byte_operands.resize(
512 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
521 num_elements = *max_bytes;
525 for(
mp_integer i = first_element; i < *num_elements; ++i)
530 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
533 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
534 element = src_simp.
operands()[index_int];
546 ? std::min(
mp_integer{el_bytes}, *max_bytes - byte_operands.size())
548 const std::size_t element_max_bytes_int =
549 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
553 unpack_rec(element, little_endian, {}, element_max_bytes, ns,
true);
556 byte_operands.insert(
557 byte_operands.end(), sub_operands.begin(), sub_operands.end());
559 if(max_bytes && byte_operands.size() >= *max_bytes)
563 const std::size_t size = byte_operands.size();
565 std::move(byte_operands),
581 std::size_t total_bits,
592 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns,
true);
596 std::make_move_iterator(sub.
operands().begin()),
597 std::make_move_iterator(sub.
operands().end()));
625 for(
auto it = components.begin(); it != components.end(); ++it)
627 const auto &comp = *it;
636 component_bits.has_value() ||
637 (std::next(it) == components.end() && !bit_fields.has_value()),
638 "members of non-constant width should come last in a struct");
641 if(src.
id() == ID_struct)
647 if(bit_fields.has_value())
650 std::move(bit_fields->first),
660 if(offset_bytes.has_value())
665 if(*offset_in_member < 0)
666 offset_in_member.reset();
669 if(max_bytes.has_value())
672 if(*max_bytes_left < 0)
679 (component_bits.has_value() && *component_bits % 8 != 0))
681 if(!bit_fields.has_value())
684 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
685 bit_fields->first.insert(
686 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
688 bit_fields->second += bits_int;
696 !bit_fields.has_value(),
697 "all preceding members should have been processed");
700 member, little_endian, offset_in_member, max_bytes_left, ns,
true);
702 byte_operands.insert(
704 std::make_move_iterator(sub.
operands().begin()),
705 std::make_move_iterator(sub.
operands().end()));
707 if(component_bits.has_value())
711 if(bit_fields.has_value())
713 std::move(bit_fields->first),
721 const std::size_t size = byte_operands.size();
757 byte_operands.insert(
759 std::make_move_iterator(sub_imag.
operands().begin()),
760 std::make_move_iterator(sub_imag.
operands().end()));
762 const std::size_t size = byte_operands.
size();
784 bool unpack_byte_array)
786 if(src.
type().
id()==ID_array)
794 if(!unpack_byte_array && *element_bits == 8)
797 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
807 else if(src.
type().
id() == ID_vector)
815 if(!unpack_byte_array && *element_bits == 8)
820 numeric_cast_v<mp_integer>(vector_type.
size()),
827 else if(src.
type().
id() == ID_complex)
831 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
833 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
835 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
844 for(
const auto &comp : components)
848 if(!element_width.has_value() || *element_width <= max_width)
851 max_width = *element_width;
852 max_comp_type = comp.type();
853 max_comp_name = comp.get_name();
860 member, little_endian, offset_bytes, max_bytes, ns,
true);
863 else if(src.
type().
id() == ID_pointer)
873 else if(src.
id() == ID_string_constant)
883 else if(src.
id() == ID_constant && src.
type().
id() == ID_string)
893 else if(src.
type().
id()!=ID_empty)
898 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
904 if(max_bytes.has_value())
906 const auto max_bits = *max_bytes * 8;
909 last_bit = std::min(last_bit, max_bits);
913 bit_offset = std::max(
mp_integer{0}, last_bit - max_bits);
918 src,
bv_typet{numeric_cast_v<std::size_t>(total_bits)});
921 for(; bit_offset < last_bit; bit_offset += 8)
933 byte_operands.push_back(extractbits);
935 byte_operands.insert(byte_operands.begin(), extractbits);
938 const std::size_t size = byte_operands.size();
940 std::move(byte_operands),
965 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
970 real.
type() = subtype;
976 imag.
type() = subtype;
1035 src.
id() == ID_byte_extract_little_endian ||
1036 src.
id() == ID_byte_extract_big_endian);
1037 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
1041 if(upper_bound_opt.has_value())
1045 upper_bound_opt.value(),
1047 src.
offset(), upper_bound_opt.value().
type())),
1050 else if(src.
type().
id() == ID_empty)
1053 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
1054 const auto upper_bound_int_opt =
1055 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
1059 src.
op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1064 if(src.
type().
id()==ID_array)
1073 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1075 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
1077 if(num_elements.has_value())
1080 operands.reserve(*num_elements);
1081 for(std::size_t i = 0; i < *num_elements; ++i)
1088 tmp.
type() = subtype;
1089 tmp.
offset() = new_offset;
1100 static std::size_t array_comprehension_index_counter = 0;
1101 ++array_comprehension_index_counter;
1103 "$array_comprehension_index_a" +
1112 *element_bits / 8, array_comprehension_index.type())},
1116 body.
type() = subtype;
1117 body.
offset() = std::move(new_offset);
1125 else if(src.
type().
id() == ID_vector)
1134 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1136 const std::size_t num_elements =
1137 numeric_cast_v<std::size_t>(vector_type.
size());
1140 operands.reserve(num_elements);
1141 for(std::size_t i = 0; i < num_elements; ++i)
1148 tmp.
type() = subtype;
1157 else if(src.
type().
id() == ID_complex)
1160 if(result.has_value())
1161 return std::move(*result);
1165 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1173 for(
const auto &comp : components)
1179 !component_bits.has_value() || *component_bits == 0 ||
1180 *component_bits % 8 != 0)
1186 auto member_offset_opt =
1189 if(!member_offset_opt.has_value())
1198 member_offset_opt.value(), unpacked.
offset().
type()));
1201 tmp.
type()=comp.type();
1210 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1216 if(widest_member.has_value())
1219 tmp.
type() = widest_member->first.type();
1222 widest_member->first.get_name(),
1228 const exprt &root=unpacked.
op();
1232 if(root.
type().
id() == ID_vector)
1240 subtype_bits.has_value() && *subtype_bits == 8,
1241 "offset bits are byte aligned");
1244 if(!size_bits.has_value())
1249 op0_bits.has_value(),
1250 "the extracted width or the source width must be known");
1251 size_bits = op0_bits;
1254 mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1257 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1259 op.reserve(width_bytes);
1261 for(std::size_t i=0; i<width_bytes; i++)
1264 std::size_t offset_int=
1265 little_endian?(width_bytes-i-1):i;
1272 offset_i.is_constant() &&
1273 (root.
id() == ID_array || root.
id() == ID_vector) &&
1275 index < root.
operands().size() && index >= 0)
1278 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1303 const exprt &value_as_byte_array,
1318 const typet &subtype,
1319 const exprt &value_as_byte_array,
1320 const exprt &non_const_update_bound,
1325 static std::size_t array_comprehension_index_counter = 0;
1326 ++array_comprehension_index_counter;
1328 "$array_comprehension_index_u_a_v" +
1334 array_comprehension_index, src.
offset().
type()),
1339 array_comprehension_index, non_const_update_bound.
type()),
1342 src.
offset(), non_const_update_bound.
type()),
1343 non_const_update_bound}};
1346 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1350 value_as_byte_array,
1353 src.
offset(), array_comprehension_index.
type())}},
1358 std::move(array_comprehension_body),
1374 const typet &subtype,
1382 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1392 if(e.id() == ID_index)
1395 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1400 if(non_const_update_bound.has_value())
1406 *non_const_update_bound},
1414 if(result.
id() != ID_with)
1415 result =
with_exprt{result, where, update_value};
1440 const typet &subtype,
1441 const exprt &subtype_size,
1442 const exprt &value_as_byte_array,
1443 const exprt &non_const_update_bound,
1444 const exprt &initial_bytes,
1445 const exprt &first_index,
1446 const exprt &first_update_value,
1449 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1450 ? ID_byte_extract_little_endian
1451 : ID_byte_extract_big_endian;
1455 static std::size_t array_comprehension_index_counter = 0;
1456 ++array_comprehension_index_counter;
1458 "$array_comprehension_index_u_a_v_u" +
1470 array_comprehension_index, first_index.
type()),
1479 array_comprehension_index, first_index.
type()),
1483 extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1492 non_const_update_bound, subtype_size.
type()),
1504 non_const_update_bound, initial_bytes.
type()),
1512 array_comprehension_index, last_index.type()),
1525 value_as_byte_array,
1527 last_index, subtype_size.
type()),
1533 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1537 array_comprehension_index, first_index.
type()),
1541 array_comprehension_index, last_index.type()),
1543 std::move(last_update_value),
1544 std::move(update_value)}}};
1548 std::move(array_comprehension_body),
1565 const typet &subtype,
1566 const exprt &value_as_byte_array,
1570 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1571 ? ID_byte_extract_little_endian
1572 : ID_byte_extract_big_endian;
1581 subtype_size_opt.value(), src.
offset().
type()),
1596 if(non_const_update_bound.has_value())
1599 *non_const_update_bound, subtype_size.
type());
1604 value_as_byte_array.
id() == ID_array,
1605 "value should be an array expression if the update bound is constant");
1623 value_as_byte_array,
1628 if(value_as_byte_array.
id() != ID_array)
1634 value_as_byte_array,
1635 *non_const_update_bound,
1647 std::size_t step_size = 1;
1654 std::size_t offset = 0;
1658 with_exprt result{src.
op(), first_index, first_update_value};
1661 for(; offset + step_size <= value_as_byte_array.
operands().size();
1662 offset += step_size, ++i)
1679 value_as_byte_array,
1680 std::move(offset_expr),
1688 if(offset < value_as_byte_array.
operands().size())
1690 const std::size_t tail_size =
1691 value_as_byte_array.
operands().size() - offset;
1703 value_as_byte_array,
1725 const typet &subtype,
1726 const exprt &value_as_byte_array,
1730 const bool is_array = src.
type().
id() == ID_array;
1742 !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1743 non_const_update_bound.has_value() || value_as_byte_array.
id() != ID_array)
1746 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1749 std::size_t num_elements =
1755 elements.reserve(num_elements);
1759 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1763 for(; i < num_elements &&
1765 (offset_bytes + value_as_byte_array.operands().size()) * 8;
1768 mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1769 mp_integer update_elements = *subtype_bits / 8;
1770 exprt::operandst::const_iterator first =
1771 value_as_byte_array.operands().begin();
1772 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1773 if(update_offset < 0)
1776 value_as_byte_array.operands().size() > -update_offset,
1777 "indices past the update should be handled above");
1778 first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1782 update_elements -= update_offset;
1784 update_elements > 0,
1785 "indices before the update should be handled above");
1788 if(std::distance(first, end) > update_elements)
1789 end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1791 const std::size_t update_size = update_values.size();
1796 from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1798 std::move(update_values),
1804 for(; i < num_elements; ++i)
1805 elements.push_back(
index_exprt{src.op(), from_integer(i, index_type())});
1827 const exprt &value_as_byte_array,
1831 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1832 ? ID_byte_extract_little_endian
1833 : ID_byte_extract_big_endian;
1836 elements.reserve(struct_type.
components().size());
1839 for(
const auto &comp : struct_type.
components())
1851 auto offset_bytes = numeric_cast<mp_integer>(offset);
1858 offset_bytes.has_value() &&
1859 (*offset_bytes * 8 >= *element_width ||
1860 (value_as_byte_array.
id() == ID_array && *offset_bytes < 0 &&
1861 -*offset_bytes >= value_as_byte_array.
operands().size())))
1863 elements.push_back(std::move(member));
1867 else if(!offset_bytes.has_value())
1890 bu, value_as_byte_array, non_const_update_bound, ns),
1900 mp_integer update_elements = (*element_width + 7) / 8;
1901 std::size_t first = 0;
1902 if(*offset_bytes < 0)
1906 value_as_byte_array.
id() != ID_array ||
1907 value_as_byte_array.
operands().size() > -*offset_bytes,
1908 "members past the update should be handled above");
1909 first = numeric_cast_v<std::size_t>(-*offset_bytes);
1913 update_elements -= *offset_bytes;
1915 update_elements > 0,
1916 "members before the update should be handled above");
1922 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1923 if(value_as_byte_array.
id() == ID_array)
1924 end = std::min(end, value_as_byte_array.
operands().size());
1927 const std::size_t update_size = update_values.size();
1936 if(non_const_update_bound.has_value())
1944 *non_const_update_bound,
1956 remaining_update_bytes};
1958 member_update_bound = std::move(update_size_expr);
1963 const std::size_t shift =
1965 const std::size_t element_bits_int =
1966 numeric_cast_v<std::size_t>(*element_width);
1968 const bool little_endian = src.
id() == ID_byte_update_little_endian;
1974 bv_typet{shift + element_bits_int}};
1983 exprt updated_element =
1987 elements.push_back(updated_element);
1992 element_bits_int - 1 + (little_endian ? shift : 0),
1993 (little_endian ? shift : 0),
2016 const exprt &value_as_byte_array,
2023 widest_member.has_value(),
2024 "lower_byte_update of union of unknown size is not supported");
2028 src.
op(), widest_member->first.get_name(), widest_member->first.
type()});
2029 bu.
type() = widest_member->first.type();
2032 widest_member->first.get_name(),
2047 const exprt &value_as_byte_array,
2051 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
2054 if(src.
type().
id() == ID_vector)
2064 if(*element_width == 8)
2066 if(value_as_byte_array.
id() != ID_array)
2069 non_const_update_bound.has_value(),
2070 "constant update bound should yield an array expression");
2072 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2079 non_const_update_bound,
2084 src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2086 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
2091 value_as_byte_array,
2092 non_const_update_bound,
2097 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
2102 value_as_byte_array,
2103 non_const_update_bound,
2110 src.
type().
id() == ID_c_enum || src.
type().
id() == ID_c_enum_tag)
2115 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2116 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2119 if(value_as_byte_array.
id() == ID_array)
2120 update_bytes = value_as_byte_array.
operands();
2127 const std::size_t update_size_bits = update_bytes.size() * 8;
2128 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2130 const bool is_little_endian = src.
id() == ID_byte_update_little_endian;
2134 if(bit_width > type_bits)
2141 if(!is_little_endian)
2147 if(non_const_update_bound.has_value())
2151 src.
id() == ID_byte_update_little_endian,
2157 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2163 *non_const_update_bound},
2171 if(is_little_endian)
2176 power(2, bit_width) -
power(2, bit_width - update_size_bits),
2184 offset_times_eight, ID_ge,
from_integer(0, offset_type)};
2186 if_exprt mask_shifted{offset_ge_zero,
2189 if(!is_little_endian)
2190 mask_shifted.true_case().
swap(mask_shifted.false_case());
2197 if(is_little_endian)
2198 std::reverse(value.operands().begin(), value.operands().end());
2200 exprt zero_extended;
2201 if(bit_width > update_size_bits)
2208 if(!is_little_endian)
2214 zero_extended = value;
2217 if_exprt value_shifted{offset_ge_zero,
2218 shl_exprt{zero_extended, offset_times_eight},
2219 lshr_exprt{zero_extended, offset_times_eight}};
2220 if(!is_little_endian)
2221 value_shifted.true_case().
swap(value_shifted.false_case());
2224 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2226 if(!is_little_endian && bit_width > type_bits)
2232 bit_width - type_bits,
2237 else if(bit_width > 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)