[depends: #1161, #1272] JSON expr and JSON trace

regression/cbmc-java/address_space_size_limit1/Test.java

@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}

regression/cbmc-java/address_space_size_limit1/test.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--object-bits 4
+too many addressed objects
+--

regression/cbmc-java/address_space_size_limit2/Test.java

@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}

regression/cbmc-java/address_space_size_limit2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--object-bits 8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::Test.main:\(\[Ljava/lang/String;\)V.assertion.1\] .*: FAILURE$
+--

regression/cbmc-java/exceptions20/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.class
+--json-ui --trace
+^EXIT=10$
+^SIGNAL=0$
+.*VERIFICATION FAILED.*
+--
+^warning: ignoring
+--
+this fails with assertion error if nil values are not allowed in assignments in
+the JSON trace

regression/cbmc-java/exceptions20/test.java

@@ -0,0 +1,30 @@
+class A extends Throwable {}
+class B extends A {}
+class C extends B {}
+class D extends C {}
+
+public class test {
+ public static void main (String arg[]) {
+   try {
+     D d = new D();
+     C c = new C();
+     B b = new B();
+     A a = new A();
+     A e = a;
+     throw e;
+   }
+   catch(D exc) {
+     assert false;
+   }
+   catch(C exc) {
+     assert false;
+   }
+   catch(B exc) {
+     assert false;
+   }
+   catch(A exc) {
+     assert false;
+   }  
+ }
+}
+

regression/cbmc-java/json_trace1/Test.java

@@ -0,0 +1,21 @@
+public class Test {
+
+  byte main(byte[] a) {
+    if (a.length != 9) {
+      return -1;
+    }
+
+    byte diff = 0;
+    for (byte i = 0; i < 9; i++) {
+      if (a[i] == 1) {
+        diff++;
+      } else if (a[i] == 2) {
+        diff--;
+      } else if (a[i] != 0) {
+        return -1;
+      }
+    }
+
+    return -1;
+  }
+}

regression/cbmc-java/json_trace1/test.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--cover location --trace --json-ui
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/json_trace2/Test.java

@@ -0,0 +1,7 @@
+public class Test {
+  boolean test(Object x) {
+    if(x==null)
+      return false;
+    return true;
+  }
+}

regression/cbmc-java/json_trace2/test.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--cover location --trace --json-ui --function Test.test
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8
+"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; boolean @lock; \} \*"
+--
+^warning: ignoring

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,5 +1,5 @@
 CORE
 test.c
---no-simplify --unwind 300
-too many variables
+--no-simplify --unwind 300 --object-bits 8
+too many addressed objects
 --

regression/cbmc/address_space_size_limit2/test.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+  char* c=(char*)malloc(10);
+  char* d=c;
+  for(char i=0; i<10; i++, d++);
+  assert((size_t)d==(size_t)c+10);
+}

regression/cbmc/address_space_size_limit2/test.desc

@@ -0,0 +1,5 @@
+KNOWNBUG
+test.c
+--32 --object-bits 31 --unwind 11 --no-simplify
+dynamic object too large
+--

regression/cbmc/address_space_size_limit3/main.c

@@ -0,0 +1,136 @@
+// copy of Pointer_Arithmetic12
+
+#include <stdint.h>
+
+#include <assert.h>
+
+uint32_t __stack[32];
+
+uint32_t eax;
+uint32_t ebp;
+uint32_t ebx;
+uint32_t ecx;
+uint32_t edi;
+uint32_t edx;
+uint32_t esi;
+uint32_t esp=(uint32_t)&(__stack[31]);
+uint32_t var0;
+uint32_t var1;
+uint32_t var10;
+uint32_t var11;
+uint32_t var12;
+uint32_t var13;
+uint32_t var14;
+uint32_t var15;
+uint32_t var16;
+uint32_t var2;
+uint32_t var3;
+uint32_t var4;
+uint32_t var5;
+uint32_t var6;
+uint32_t var7;
+uint32_t var8;
+uint32_t var9;
+
+void g__L_0x3b4_0()
+{
+  L_0x3b4_0: esp-=0x4;
+  L_0x3b4_1: *(uint32_t*)(esp)=ebp;
+  L_0x3b5_0: ebp=esp;
+  L_0x3b7_0: var4=ebp;
+  L_0x3b7_1: var4+=0xc;
+  L_0x3b7_2: eax=*(uint32_t*)(var4);
+  L_0x3ba_0: edx=eax;
+  L_0x3bc_0: edx&=0x3;
+  L_0x3bf_0: var5=ebp;
+  L_0x3bf_1: var5+=0x8;
+  L_0x3bf_2: eax=*(uint32_t*)(var5);
+  L_0x3c2_0: *(uint32_t*)(eax)=edx;
+  L_0x3c4_0: ebp=*(uint32_t*)(esp);
+  L_0x3c4_1: esp+=0x4;
+  L_0x3c5_0: return;
+}
+
+void f__L_0x3c6_0()
+{
+  L_0x3c6_0: esp-=0x4;
+  L_0x3c6_1: *(uint32_t*)(esp)=ebp;
+  L_0x3c7_0: ebp=esp;
+  L_0x3c9_0: esp-=0x18;
+  L_0x3cc_0: var6=ebp;
+  L_0x3cc_1: var6-=0x4;
+  L_0x3cc_2: *(uint32_t*)(var6)=0x0;
+  L_0x3d3_0: var7=ebp;
+  L_0x3d3_1: var7-=0x8;
+  L_0x3d3_2: *(uint32_t*)(var7)=0x0;
+  L_0x3da_0: var8=ebp;
+  L_0x3da_1: var8+=0x8;
+  L_0x3da_2: eax=*(uint32_t*)(var8);
+  L_0x3dd_0: var9=ebp;
+  L_0x3dd_1: var9-=0x4;
+  L_0x3dd_2: *(uint32_t*)(var9)=eax;
+  L_0x3e0_0: var10=ebp;
+  L_0x3e0_1: var10-=0x4;
+  L_0x3e0_2: eax=*(uint32_t*)(var10);
+  L_0x3e3_0: var11=esp;
+  L_0x3e3_1: var11+=0x4;
+  L_0x3e3_2: *(uint32_t*)(var11)=eax;
+  L_0x3e7_0: var12=ebp;
+  L_0x3e7_1: var12-=0x8;
+  L_0x3e7_2: eax=(uint32_t)&*(uint32_t*)(var12);
+  L_0x3ea_0: *(uint32_t*)(esp)=eax;
+  L_0x3ed_0: esp-=4; g__L_0x3b4_0(); esp+=4;
+  L_0x3f2_0: var13=ebp;
+  L_0x3f2_1: var13-=0x4;
+  L_0x3f2_2: *(uint32_t*)(var13)=0x5;
+  L_0x3f9_0: var14=ebp;
+  L_0x3f9_1: var14-=0x8;
+  L_0x3f9_2: eax=*(uint32_t*)(var14);
+  L_0x3fc_0: esp=ebp;
+  L_0x3fc_1: ebp=*(uint32_t*)(esp);
+  L_0x3fc_2: esp+=0x4;
+  L_0x3fd_0: return;
+}
+
+int main()
+{
+  L_0x3fe_0: esp-=0x4;
+  L_0x3fe_1: *(uint32_t*)(esp)=ebp;
+  L_0x3ff_0: ebp=esp;
+  L_0x401_0: esp-=0x14;
+  L_0x404_0: var15=ebp;
+  L_0x404_1: var15-=0x4;
+#ifdef NONDET
+  L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
+#else
+  L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
+#endif
+  L_0x40b_0: var16=ebp;
+  L_0x40b_1: var16-=0x4;
+  L_0x40b_2: eax=*(uint32_t*)(var16);
+  L_0x40e_0: *(uint32_t*)(esp)=eax;
+  L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
+#if 1
+             uint32_t eax1=eax;
+  C_0x3ff_0: ebp=esp;
+  C_0x401_0: esp-=0x14;
+  C_0x404_0: var15=ebp;
+  C_0x404_1: var15-=0x4;
+#ifdef NONDET
+  C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
+#else
+  C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
+#endif
+  C_0x40b_0: var16=ebp;
+  C_0x40b_1: var16-=0x4;
+  C_0x40b_2: eax=*(uint32_t*)(var16);
+  C_0x40e_0: *(uint32_t*)(esp)=eax;
+  C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
+             uint32_t eax2=eax;
+             assert(eax2==eax1);
+#endif
+  L_0x416_0: esp=ebp;
+  L_0x416_1: ebp=*(uint32_t*)(esp);
+  L_0x416_2: esp+=0x4;
+  L_0x417_0: return 0;
+}

regression/cbmc/address_space_size_limit3/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--32 --little-endian --object-bits 25 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^.* dereference failure: pointer outside object bounds in .*: FAILURE$
+--
+^warning: ignoring
+--
+requires at least 8 offset bits

regression/cbmc/trace_class_identifier/TestGenTest.java

@@ -0,0 +1,7 @@
+public class TestGenTest
+{
+  public void f()
+  {
+    int a = 4;
+  }
+}

regression/cbmc/trace_class_identifier/test.desc

@@ -0,0 +1,8 @@
+CORE
+TestGenTest.class
+--function TestGenTest.f --trace --cover location --json-ui
+"data": "java::TestGenTest",$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/strings-smoke-tests/jsonArrays/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+--refine-strings --function test.check --json-ui --trace --string-max-length 100 --cover location
+^EXIT=0$
+^SIGNAL=0$
+\"data\".*\"tmp_object_factory\$6.*\"
+--
+This checks that tmp_object_factory$6 gets affected to the data field
+of some strings, which was not the case in previous versions of cbmc,
+as it was just ignored by the json output.

regression/strings-smoke-tests/jsonArrays/test.java

@@ -0,0 +1,8 @@
+public class test
+{
+    public static int check(String s)
+    {
+        int i=Integer.parseInt(s);
+        return i;
+    }
+}

src/cbmc/bmc_cover.cpp

@@ -393,7 +393,8 @@ bool bmc_covert::operator()()
               json_objectt json_input;
               json_input["id"]=json_stringt(id2string(step.io_id));
               if(step.io_args.size()==1)
-                json_input["value"]=json(step.io_args.front(), bmc.ns);
+                json_input["value"]=
+                  json(step.io_args.front(), bmc.ns, ID_unknown);
               json_test.push_back(json_input);
             }
           }