Crashing test cases due to pointer arithmetic issues.

Author: martin

regression/goto-analyzer/variable-sensitivity-bug-02/main.c

@@ -0,0 +1,34 @@
+// map.c
+int map(int t_x, int * p_map)   // mismatch :(
+{
+  int n = p_map[0];
+  int *p_map_x = &p_map[1];
+  int *p_map_y = p_map_x + n ;  // assertion failed here
+  int i;
+
+  if (t_x < p_map_x[0])
+    return p_map_y[0];
+
+  for (i=1; i<n; i++)
+    if (t_x < p_map_x[i])
+    {
+      int x0 = p_map_x[i-1];
+      int x1 = p_map_x[i];
+      int y0 = p_map_y[i-1];
+      int y1 = p_map_y[i];
+      return (y1-y0)/(x1-x0) * (t_x-x0) + y0;
+    }
+
+  return p_map_y[n-1];
+}
+
+/// file2.c
+int map(int t_x, volatile const int* p_map);
+volatile const int s_map_data[] = { 2, 10, 20, 100, 110 };
+extern int g_x;
+int g_y;
+
+void main(void)
+{
+   g_y = map(g_x, s_map_data);
+}

regression/goto-analyzer/variable-sensitivity-bug-02/test.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+main.c
+--variable-sensitivity --structs --arrays --pointers --show
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/variable-sensitivity-bug-03/main.c

@@ -0,0 +1,7 @@
+void main(void)
+{
+  const int s_map_data[] = { 2, 10, 20, 100, 110 };
+
+  int *p_map_x = &s_map_data[1];
+  int *p_map_y = p_map_x + 1 ;  // assertion failed here  
+}

regression/goto-analyzer/variable-sensitivity-bug-03/test.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+main.c
+--variable-sensitivity --structs --arrays --pointers --show
+^EXIT=0$
+^SIGNAL=0$
+--

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -230,7 +230,10 @@ bool abstract_environmentt::assign(
   const typet &rhs_type=ns.follow(final_value->type());
 
   // Write the value for the root symbol back into the map
-  INVARIANT(lhs_type==rhs_type, "Assignment types must match");
+  INVARIANT(lhs_type==rhs_type,
+            "Assignment types must match" "\n"
+            "lhs_type :" + lhs_type.pretty() + "\n"
+            "rhs_type :" + rhs_type.pretty());
   // If LHS was directly the symbol
   if(s.id()==ID_symbol)
   {