Hardwire maximum array size

Author: jezhiggins

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -24,6 +24,8 @@ struct eval_index_resultt
   mp_integer value;
 };
 
+static mp_integer max_array_index = 10;
+
 static eval_index_resultt eval_index(
   const exprt &expr,
   const abstract_environmentt &env,
@@ -453,5 +455,8 @@ static eval_index_resultt eval_index(
   mp_integer out_index;
   bool result = to_integer(to_constant_expr(value), out_index);
 
+  if(out_index > max_array_index)
+    out_index = max_array_index;
+
   return {!result, out_index};
 }

unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp

@@ -46,7 +46,7 @@ SCENARIO(
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
-  WHEN("Under maximum size, array = {1, 2, 3}")
+  WHEN("array = {1, 2, 3}, writes under maximum size")
   {
     WHEN("array[3] = 4")
     {
@@ -92,4 +92,21 @@ SCENARIO(
       }
     }
   }
+  WHEN("array = {1, 2, 3}, writes beyond maximum size mapped to max_size")
+  {
+    WHEN("array[99] = 4")
+    {
+      auto array = build_array({1, 2, 3}, environment, ns);
+
+      auto updated = write_array(array, 99, 4, environment, ns);
+
+      THEN("array equals {1, 2, 3, ..., [10] = 4}")
+      {
+        EXPECT_INDEX(updated, 0, 1, environment, ns);
+        EXPECT_INDEX(updated, 1, 2, environment, ns);
+        EXPECT_INDEX(updated, 2, 3, environment, ns);
+        EXPECT_INDEX(updated, 10, 4, environment, ns);
+      }
+    }
+  }
 }