fix for non-byte array byte_extract flattening

Author: Daniel Kroening

regression/cbmc/Pointer_array5/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Pointer_array6/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+#include <stdlib.h>
+
+extern int nondet_int();
+
+int main() {
+
+  int arraylen=nondet_int();
+
+  if(arraylen==3)
+  {
+    int** array_init = malloc(sizeof(int *)*arraylen);
+
+    // mis-align that pointer!
+    char * char_ptr = (char *) array_init;
+    char_ptr++;
+    
+    int local_var;
+
+    int **array2=(int**)char_ptr;
+    
+    // write
+    array2[0]=&local_var;
+    
+    // check
+    int value=*array2[0];
+
+    assert(value==local_var);
+  }
+
+}

regression/cbmc/Pointer_array6/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/flattening/flatten_byte_operators.cpp

@@ -117,7 +117,7 @@ exprt flatten_byte_extract(
       for(mp_integer i=0; i<num_elements; ++i)
       {
         // the most significant byte comes first in the concatenation!
-        plus_exprt index(first_index, from_integer(i, offset_type));
+        plus_exprt index(first_index, from_integer(num_elements-i-1, offset_type));
         concat.copy_to_operands(index_exprt(root, index));
       }