@@ -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,41 @@ 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+ mp_vectort extract_from;
920+ evaluate (expr.op0 (), extract_from);
921+ INVARIANT (
922+ !extract_from.empty (),
923+ " evaluate_address should have returned address == 0" );
924+ const mp_integer memory_offset =
925+ address - evaluate_address (expr.op0 (), true );
926+ const typet &target_type = expr.type ();
927+ mp_integer target_type_leaves;
928+ if (!count_type_leaves (target_type, target_type_leaves) &&
929+ target_type_leaves > 0 )
930+ {
931+ dest.insert (
932+ dest.end (),
933+ extract_from.begin () + numeric_cast_v<std::size_t >(memory_offset),
934+ extract_from.begin () +
935+ numeric_cast_v<std::size_t >(memory_offset + target_type_leaves));
936+ return ;
937+ }
938+ // we fail
939+ }
946940 if (!unbounded_size (expr.type ()))
947941 {
948942 dest.resize (integer2size_t (get_size (expr.type ())));
949943 read (address, dest);
944+ return ;
950945 }
951946 else
952947 {
953948 read_unbounded (address, dest);
949+ return ;
954950 }
955- return ;
956951 }
957952 }
958953 else if (expr.id ()==ID_typecast)
0 commit comments