@@ -857,41 +857,11 @@ void interpretert::evaluate(
857857 }
858858 return ;
859859 }
860- else if (expr.id ()==ID_byte_extract_little_endian ||
861- expr.id ()==ID_byte_extract_big_endian)
862- {
863- const auto &byte_extract_expr = to_byte_extract_expr (expr);
864-
865- mp_vectort extract_offset;
866- evaluate (byte_extract_expr.op1 (), extract_offset);
867- mp_vectort extract_from;
868- evaluate (byte_extract_expr.op0 (), extract_from);
869-
870- if (extract_offset.size ()==1 && extract_from.size ()!=0 )
871- {
872- const typet &target_type=expr.type ();
873- mp_integer memory_offset;
874- // If memory offset is found (which should normally be the case)
875- // extract the corresponding data from the appropriate memory location
876- if (!byte_offset_to_memory_offset (
877- byte_extract_expr.op0 ().type (), extract_offset[0 ], memory_offset))
878- {
879- mp_integer target_type_leaves;
880- if (!count_type_leaves (target_type, target_type_leaves) &&
881- target_type_leaves>0 )
882- {
883- dest.insert (dest.end (),
884- extract_from.begin ()+memory_offset.to_long (),
885- extract_from.begin ()+(memory_offset+target_type_leaves).to_long ());
886- return ;
887- }
888- }
889- }
890- }
891- else if (expr.id ()==ID_dereference ||
892- expr.id ()==ID_index ||
893- expr.id ()==ID_symbol ||
894- expr.id ()==ID_member)
860+ else if (
861+ expr.id () == ID_dereference || expr.id () == ID_index ||
862+ expr.id () == ID_symbol || expr.id () == ID_member ||
863+ expr.id () == ID_byte_extract_little_endian ||
864+ expr.id () == ID_byte_extract_big_endian)
895865 {
896866 mp_integer address=evaluate_address (
897867 expr,
@@ -932,16 +902,45 @@ void interpretert::evaluate(
932902 }
933903 else if (!address.is_zero ())
934904 {
935- if (!unbounded_size (expr.type ()))
905+ if (
906+ expr.id () == ID_byte_extract_little_endian ||
907+ expr.id () == ID_byte_extract_big_endian)
908+ {
909+ const auto &byte_extract_expr = to_byte_extract_expr (expr);
910+
911+ mp_vectort extract_from;
912+ evaluate (byte_extract_expr.op (), extract_from);
913+ INVARIANT (
914+ !extract_from.empty (),
915+ " evaluate_address should have returned address == 0" );
916+ const mp_integer memory_offset =
917+ address - evaluate_address (byte_extract_expr.op (), true );
918+ const typet &target_type = expr.type ();
919+ mp_integer target_type_leaves;
920+ if (
921+ !count_type_leaves (target_type, target_type_leaves) &&
922+ target_type_leaves > 0 )
923+ {
924+ dest.insert (
925+ dest.end (),
926+ extract_from.begin () + numeric_cast_v<std::size_t >(memory_offset),
927+ extract_from.begin () +
928+ numeric_cast_v<std::size_t >(memory_offset + target_type_leaves));
929+ return ;
930+ }
931+ // we fail
932+ }
933+ else if (!unbounded_size (expr.type ()))
936934 {
937935 dest.resize (numeric_cast_v<std::size_t >(get_size (expr.type ())));
938936 read (address, dest);
937+ return ;
939938 }
940939 else
941940 {
942941 read_unbounded (address, dest);
942+ return ;
943943 }
944- return ;
945944 }
946945 }
947946 else if (expr.id ()==ID_typecast)
0 commit comments