Merge pull request #390 from smowton/clean_vla_size

Clean variable-length array size expressions. Fixes verification-engine-utils#192

Author: Daniel Kroening

regression/cbmc-java/VarLengthArrayTrace1/Container.class

@@ -0,0 +1,21 @@
+public class VarLengthArrayTrace1 {
+
+  public static void main(int unknown, int arg2) {
+
+    Container c = new Container(unknown);
+    if(c.val != 2) return;
+    int[] arr = new int[c.val];
+    arr[1] = arg2;
+    int test = arr[1];
+    assert(test != 10);
+
+  }
+
+}
+
+class Container {
+
+  public Container(int v) { val = v; }
+  int val;
+
+}

regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class

@@ -0,0 +1,10 @@
+CORE
+VarLengthArrayTrace1.class
+--trace
+^EXIT=10$
+^SIGNAL=0$
+dynamic_3_array\[1l\]=10
+--
+^warning: ignoring
+assignment removed
+irep("(\\"nil\\")")

regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java

@@ -478,7 +478,9 @@ void goto_symext::symex_cpp_new(
   {
     symbol.type=array_typet();
     symbol.type.subtype()=code.type().subtype();
-    symbol.type.set(ID_size, code.find(ID_size));
+    exprt size_arg=static_cast<const exprt&>(code.find(ID_size));
+    clean_expr(size_arg, state, false);
+    symbol.type.set(ID_size, size_arg);
   }
   else
     symbol.type=code.type().subtype();