Merge pull request #5334 from thk123/make-min-unwind-consistent-with-unwind

Make min unwind consistent with unwind

Author: Thomas Kiley

regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind0.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 0
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ property: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This test correctly fails because the first iteration of the loop violates the
+property.

regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind1.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ property: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This test correctly fails because the first iteration of the loop violates the
+property.

regression/cbmc-incr-oneloop/ignore-before-unwind/skip_first_unwind.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1
+--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/goto-checker/bmc_util.h

@@ -221,6 +221,11 @@ void run_property_decider(
   "                              of loop L\n" \
   "                              (use --show-loops to get the loop IDs)\n" \
   " --unwind-min nr              start incremental-loop after nr unwindings\n" \
+  "                              but before solving that iteration. If for\n" \
+  "                              example it is 1, then the loop will be\n" \
+  "                              unwound once, and immediately checked.\n" \
+  "                              Note: this means for min-unwind 1 or\n"\
+  "                              0 all properties are checked.\n" \
   " --unwind-max nr              stop incremental-loop after nr unwindings\n" \
   " --ignore-properties-before-unwind-min\n" \
   "                              do not check properties before unwind-min\n" \

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -37,8 +37,12 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
                                    : 0),
     output_ui(output_ui)
 {
+  // the intended behaviour is to stop asserts that are violated before the
+  // unwind
+  // therefore if the min-unwind is 1, then we do one unwind and immediately
+  // start checking for properties
   ignore_assertions =
-    incr_min_unwind >= 1 &&
+    incr_min_unwind > 1 &&
     options.get_bool_option("ignore-properties-before-unwind-min");
 }