Merge pull request #5820 from tautschnig/negative-byte-extract

Byte extract with negative offset must not fail invariant

Author: kroening

regression/cbmc/byte_extract1/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  int x;
+  int *p = (char *)&x - 2;
+  int y;
+  memcpy(&y, p, sizeof(int));
+  assert(0);
+}

regression/cbmc/byte_extract1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Invariant check failed
+--
+This example previously failed the invariant "mp_integer should be convertible
+to target integral type".

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -121,7 +121,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       if(offset + i < 0 || offset + i >= op_bv.size())
         bv[i]=prop.new_variable();
       else
-        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
+        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset + i)];
   }
   else
   {