Merge pull request #4372 from thk123/invalid-trace-dynamic-array

Add test verifying no invalid trace with dynamic array

Author: Thomas Kiley

jbmc/regression/jbmc/nondet-array-size/TestClass.class

@@ -0,0 +1,11 @@
+import org.cprover.CProver;
+
+public class TestClass {
+
+    public static void minimalJbmc(Object[] a) {
+        CProver.assume(a != null && a.length > 1);
+        float[] assigned = new float[a.length];
+        assigned[0] = 1.0f;
+        assert(false);
+    }
+}

jbmc/regression/jbmc/nondet-array-size/TestClass.java

@@ -0,0 +1,16 @@
+CORE
+TestClass.class
+--function "TestClass.minimalJbmc" --unwind 5 --max-nondet-string-length 10 --java-unwind-enum-static --trace --json-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+--
+Verify that when an array's size is determined by an array input, the resulting
+trace is valid.
+To compile this source file, use:
+
+```bash
+$ javac -g TestClass.java -cp ../../../lib/java-models-library/target/classes/:.
+```
+to have the cprover library on the class path.

jbmc/regression/jbmc/nondet-array-size/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --json-ui --function test --trace
 activate-multi-line-match

regression/cbmc/enum-trace1/test_json.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --json-ui --stop-on-fail
 activate-multi-line-match

regression/cbmc/json1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --trace --json-ui --trace-json-extended
 ^EXIT=10$

regression/cbmc/trace_options_json_extended/extended.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --trace --json-ui
 ^EXIT=10$

regression/cbmc/trace_options_json_extended/non-extended.desc

@@ -118,6 +118,10 @@ void convert_decl(
   const symbolt *symbol;
   irep_idt base_name, display_name;
 
+  DATA_INVARIANT(
+    step.full_lhs_value.is_not_nil(),
+    "full_lhs_value in assignment must not be nil");
+
   if(!ns.lookup(identifier, symbol))
   {
     base_name = symbol->base_name;
@@ -132,9 +136,6 @@ void convert_decl(
   }
   else
   {
-    DATA_INVARIANT(
-      step.full_lhs_value.is_not_nil(),
-      "full_lhs_value in assignment must not be nil");
     full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
   }