Merge pull request #5316 from thk123/print-status-during-incremental-solving

Incremental solving producing cprover status as it goes

Author: NlightNFotis

regression/cbmc-incr-oneloop/alarm1/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
 --incremental-loop main.0 --unwind-max 15
+activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 15
 --
 ^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test-json-output.desc

@@ -5,5 +5,6 @@ main.c
 ^SIGNAL=0$
 "messageText": "VERIFICATION FAILED"
 "currentUnwinding": 1
+"incrementalStatus": "INCONCLUSIVE"
 --
 ^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc

@@ -6,5 +6,6 @@ main.c
 <text>VERIFICATION FAILED</text>
 <current-unwinding>1</current-unwinding>
 <refinement-iteration>1</refinement-iteration>
+<incremental-status>INCONCLUSIVE</incremental-status>
 --
 ^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test.desc

@@ -1,9 +1,15 @@
 CORE
 main.c
 --incremental-loop main.0 --unwind-min 5 --unwind-max 10
+activate-multi-line-match
 Current unwinding: 1
+Incremental status: INCONCLUSIVE
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 7
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+The multi-line match is added to verify that an incremental status is printed immediately after each unwinding

regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc

@@ -0,0 +1,18 @@
+CORE
+test.c
+--incremental-loop main.0 --no-propagation
+activate-multi-line-match
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
+Incremental status: FAILURE\nCurrent unwinding: 7
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Ensure that with multiple properties, the incremental status
+switches to failure as soon as one property has been falsified
+but keeps unwinding till it has resolved them all
+
+Use `--no-propagation` to ensure that even the output is the same regardless of whether the asserts are checked via the solver or the constant propagator

regression/cbmc-incr-oneloop/multiple-asserts/test.c

@@ -0,0 +1,9 @@
+int main()
+{
+  for(int i = 0; i < 10; ++i)
+  {
+    assert(i != 5);
+    assert(i != 8);
+  }
+  return 0;
+}

regression/cbmc-incr-oneloop/multiple-asserts/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--incremental-loop main.0
+activate-multi-line-match
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
+Incremental status: FAILURE\nCurrent unwinding: 7
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Ensure that with multiple properties, the incremental status
+switches to failure as soon as one property has been falsified
+but keeps unwinding till it has resolved them all

regression/cbmc-incr-oneloop/no-asserts/test.c

@@ -0,0 +1,8 @@
+int main()
+{
+  for(int i = 0; i < 10; ++i)
+  {
+  }
+  // nothing to check
+  return 0;
+}

regression/cbmc-incr-oneloop/no-asserts/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-loop main.0
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+Incremental status
+--
+Verify no incremental status updates when no properties to check

regression/cbmc-incr-oneloop/valid-asserts/test.c

@@ -0,0 +1,8 @@
+int main()
+{
+  for(int i = 0; i < 10; ++i)
+  {
+    assert(i != 10);
+  }
+  return 0;
+}