@@ -885,42 +885,11 @@ void interpretert::evaluate(
885885 }
886886 return ;
887887 }
888- else if (expr.id ()==ID_byte_extract_little_endian ||
889- expr.id ()==ID_byte_extract_big_endian)
890- {
891- if (expr.operands ().size ()!=2 )
892- throw " byte_extract should have two operands" ;
893- mp_vectort extract_offset;
894- evaluate (expr.op1 (), extract_offset);
895- mp_vectort extract_from;
896- evaluate (expr.op0 (), extract_from);
897- if (extract_offset.size ()==1 && extract_from.size ()!=0 )
898- {
899- const typet &target_type=expr.type ();
900- mp_integer memory_offset;
901- // If memory offset is found (which should normally be the case)
902- // extract the corresponding data from the appropriate memory location
903- if (!byte_offset_to_memory_offset (
904- expr.op0 ().type (),
905- extract_offset[0 ],
906- memory_offset))
907- {
908- mp_integer target_type_leaves;
909- if (!count_type_leaves (target_type, target_type_leaves) &&
910- target_type_leaves>0 )
911- {
912- dest.insert (dest.end (),
913- extract_from.begin ()+memory_offset.to_long (),
914- extract_from.begin ()+(memory_offset+target_type_leaves).to_long ());
915- return ;
916- }
917- }
918- }
919- }
920- else if (expr.id ()==ID_dereference ||
921- expr.id ()==ID_index ||
922- expr.id ()==ID_symbol ||
923- expr.id ()==ID_member)
888+ else if (
889+ expr.id () == ID_dereference || expr.id () == ID_index ||
890+ expr.id () == ID_symbol || expr.id () == ID_member ||
891+ expr.id () == ID_byte_extract_little_endian ||
892+ expr.id () == ID_byte_extract_big_endian)
924893 {
925894 mp_integer address=evaluate_address (
926895 expr,
@@ -959,16 +928,43 @@ void interpretert::evaluate(
959928 }
960929 else if (!address.is_zero ())
961930 {
931+ if (
932+ expr.id () == ID_byte_extract_little_endian ||
933+ expr.id () == ID_byte_extract_big_endian)
934+ {
935+ mp_vectort extract_from;
936+ evaluate (expr.op0 (), extract_from);
937+ INVARIANT (
938+ !extract_from.empty (),
939+ " evaluate_address should have returned address == 0" );
940+ const mp_integer memory_offset =
941+ address - evaluate_address (expr.op0 (), true );
942+ const typet &target_type = expr.type ();
943+ mp_integer target_type_leaves;
944+ if (
945+ !count_type_leaves (target_type, target_type_leaves) &&
946+ target_type_leaves > 0 )
947+ {
948+ dest.insert (
949+ dest.end (),
950+ extract_from.begin () + numeric_cast_v<std::size_t >(memory_offset),
951+ extract_from.begin () +
952+ numeric_cast_v<std::size_t >(memory_offset + target_type_leaves));
953+ return ;
954+ }
955+ // we fail
956+ }
962957 if (!unbounded_size (expr.type ()))
963958 {
964959 dest.resize (numeric_cast_v<std::size_t >(get_size (expr.type ())));
965960 read (address, dest);
961+ return ;
966962 }
967963 else
968964 {
969965 read_unbounded (address, dest);
966+ return ;
970967 }
971- return ;
972968 }
973969 }
974970 else if (expr.id ()==ID_typecast)
0 commit comments