[depends: #472] Variable Sensitivity Domain

regression/goto-analyzer/constant_assertions_01/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int nondet_int (void);
+
+int main (int argc, char **argv)
+{
+  int x = nondet_int();
+  int y = nondet_int();
+
+  __CPROVER_assert(0, "0");
+  __CPROVER_assert(0 && 1, "0 && 1");
+  __CPROVER_assert(0 || 0, "0 || 0");
+  __CPROVER_assert(0 && x, "0 && x");
+  __CPROVER_assert(y && 0, "y && 0");
+
+  return 0;
+}

regression/goto-analyzer/constant_assertions_01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --variable
+^\[main.assertion.1\] file main.c .* 0: Failure \(if reachable\)$
+^\[main.assertion.2\] file main.c .* 0 && 1: Failure \(if reachable\)$
+^\[main.assertion.3\] file main.c .* 0 || 0: Failure \(if reachable\)$
+^\[main.assertion.4\] file main.c .* 0 && x: Failure \(if reachable\)$
+^\[main.assertion.5\] file main.c .* y && 0: Failure \(if reachable\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_assertions_02/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int nondet_int (void);
+
+int main (int argc, char **argv)
+{
+  int x = nondet_int();
+  int y = nondet_int();
+
+  __CPROVER_assert(1, "1");
+  __CPROVER_assert(0 || 1, "0 || 1");
+  __CPROVER_assert(1 && 1, "1 && 1");
+  __CPROVER_assert(1 || x, "1 || x");
+  __CPROVER_assert(y || 1, "y || 1");
+
+  return 0;
+}

regression/goto-analyzer/constant_assertions_02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --variable
+^\[main\.assertion\.1\] file main\.c .* 1: Success
+^\[main\.assertion\.2\] file main\.c .* 0 || 1: Success
+^\[main\.assertion\.3\] file main\.c .* 1 && 1: Success
+^\[main\.assertion\.4\] file main\.c .* 1 || x: Success
+^\[main\.assertion\.5\] file main\.c .* y || 1: Success
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_01/constant_propagation1.c → regression/goto-analyzer/constant_propagation_01/main.c

@@ -3,12 +3,12 @@
 int main()
 {
   int i, j=20;
-  
+
   if (j==20)
   {
     int x=1,y=2,z;
     z=x+y;
-    assert(z==3);
+    __CPROVER_assert(z==3, "z==3");
   }
-    
+
 }

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -1,9 +1,9 @@
-FUTURE
-constant_propagation1.c
---constants --simplify out.goto
+CORE
+main.c
+--variable --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c → regression/goto-analyzer/constant_propagation_02/main.c

@@ -1,13 +1,12 @@
-#include <assert.h>
 
 int main()
 {
   int i=0, j=2;
 
-  if (i<50) 
+  if (i==0)
   {
     i++;
     j++;
   }
-  assert(j!=3);
+  __CPROVER_assert(j!=3, "j!=3");
 }

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -1,9 +1,9 @@
-FUTURE
-constant_propagation_02.c
---constants --simplify out.goto
+CORE
+main.c
+--variable --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c → regression/goto-analyzer/constant_propagation_03/main.c

@@ -1,13 +1,12 @@
-#include <assert.h>
 
 int main()
 {
   int i=0, j=2;
 
-  if (i==0) 
+  if (i==0)
   {
     i++;
     j++;
   }
-  assert(j!=3);
+  __CPROVER_assert(j==3, "j==3");
 }

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -1,9 +1,9 @@
-FUTURE
-constant_propagation_03.c
---constants --simplify out.goto
+CORE
+main.c
+--variable --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c → regression/goto-analyzer/constant_propagation_04/main.c

@@ -1,13 +1,12 @@
-#include <assert.h>
 
 int main()
 {
   int i=0, j=2;
 
-  if (i==0) 
+  if (i<50)
   {
     i++;
     j++;
   }
-  assert(j==3);
+  __CPROVER_assert(j==3, "j==3");
 }

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -1,9 +1,9 @@
-FUTURE
-constant_propagation_04.c
---constants --simplify out.goto
+CORE
+main.c
+--variable --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
-^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c → regression/goto-analyzer/constant_propagation_05/main.c

@@ -1,13 +1,12 @@
-#include <assert.h>
 
 int main()
 {
   int i=0, j=2;
 
-  if (i<50) 
+  if (i<50)
   {
     i++;
     j++;
   }
-  assert(j==3);
+  __CPROVER_assert(j!=3, "j!=3");
 }

regression/goto-analyzer/constant_propagation_05/test.desc

@@ -1,8 +1,8 @@
-FUTURE
-constant_propagation_05.c
---constants --verify
+CORE
+main.c
+--variable --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$
+^\[main\.assertion\.1\] .* j!=3: Failure \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_06/main.c

@@ -0,0 +1,13 @@
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<50)
+  {
+    i++;
+    j++;
+  }
+  __CPROVER_assert(i<51, "i<51");
+}
+

regression/goto-analyzer/constant_propagation_06/test.desc

@@ -1,15 +1,8 @@
-FUTURE
-constant_propagation_06.c
---intervals --verify
+CORE
+main.c
+--variable --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
-^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$
-^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$
-^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$
-^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$
-^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$
-^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$
-^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$
+^\[main.assertion.1\] .* i\s*<\s*51: Unknown$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c → regression/goto-analyzer/constant_propagation_07/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   signed int i;
@@ -17,7 +17,7 @@ int main()
         j = j + 1;
         i = i + 1;
       }
-      assert(!(i < 2));
+      __CPROVER_assert(!(i < 2), "!(i < 2)");
     }
   }
   return 0;

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -1,8 +1,9 @@
-FUTURE
-constant_propagation_07.c
---constants --verify
+KNOWNBUG
+main.c
+--variable --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 10, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
 --
 ^warning: ignoring