@@ -854,42 +854,12 @@ void interpretert::evaluate(
854854 }
855855 return ;
856856 }
857- else if (expr.id ()==ID_byte_extract_little_endian ||
858- expr.id ()==ID_byte_extract_big_endian)
859- {
860- if (expr.operands ().size ()!=2 )
861- throw " byte_extract should have two operands" ;
862- mp_vectort extract_offset;
863- evaluate (expr.op1 (), extract_offset);
864- mp_vectort extract_from;
865- evaluate (expr.op0 (), extract_from);
866- if (extract_offset.size ()==1 && extract_from.size ()!=0 )
867- {
868- const typet &target_type=expr.type ();
869- mp_integer memory_offset;
870- // If memory offset is found (which should normally be the case)
871- // extract the corresponding data from the appropriate memory location
872- if (!byte_offset_to_memory_offset (
873- expr.op0 ().type (),
874- extract_offset[0 ],
875- memory_offset))
876- {
877- mp_integer target_type_leaves;
878- if (!count_type_leaves (target_type, target_type_leaves) &&
879- target_type_leaves>0 )
880- {
881- dest.insert (dest.end (),
882- extract_from.begin ()+memory_offset.to_long (),
883- extract_from.begin ()+(memory_offset+target_type_leaves).to_long ());
884- return ;
885- }
886- }
887- }
888- }
889857 else if (expr.id ()==ID_dereference ||
890858 expr.id ()==ID_index ||
891859 expr.id ()==ID_symbol ||
892- expr.id ()==ID_member)
860+ expr.id ()==ID_member ||
861+ expr.id () == ID_byte_extract_little_endian ||
862+ expr.id () == ID_byte_extract_big_endian)
893863 {
894864 mp_integer address=evaluate_address (
895865 expr,
@@ -943,16 +913,40 @@ void interpretert::evaluate(
943913 }
944914 else if (!address.is_zero ())
945915 {
916+ if (expr.id ()==ID_byte_extract_little_endian ||
917+ expr.id ()==ID_byte_extract_big_endian)
918+ {
919+ // extract_from will be non-empty, otherwise evaluate_address would have
920+ // returned address == 0
921+ mp_vectort extract_from;
922+ evaluate (expr.op0 (), extract_from);
923+ const mp_integer memory_offset =
924+ address - evaluate_address (expr.op0 (), true );
925+ const typet &target_type = expr.type ();
926+ mp_integer target_type_leaves;
927+ if (!count_type_leaves (target_type, target_type_leaves) &&
928+ target_type_leaves > 0 )
929+ {
930+ dest.insert (
931+ dest.end (),
932+ extract_from.begin () + numeric_cast_v<std::size_t >(memory_offset),
933+ extract_from.begin () +
934+ numeric_cast_v<std::size_t >(memory_offset + target_type_leaves));
935+ return ;
936+ }
937+ // we fail
938+ }
946939 if (!unbounded_size (expr.type ()))
947940 {
948941 dest.resize (integer2size_t (get_size (expr.type ())));
949942 read (address, dest);
943+ return ;
950944 }
951945 else
952946 {
953947 read_unbounded (address, dest);
948+ return ;
954949 }
955- return ;
956950 }
957951 }
958952 else if (expr.id ()==ID_typecast)
0 commit comments