Merge pull request #8274 from tautschnig/goto-instrument-unwinding-assertions

goto-instrument/unwinding: enable unwinding assertions by default

Author: tautschnig

doc/man/cbmc.1

@@ -79,7 +79,7 @@ allow malloc calls to return a null pointer
 \fB\-\-malloc\-fail\-null\fR
 set malloc failure mode to return null
 .TP
-\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+\fB\-\-unwinding\-assertions\fR
 generate unwinding assertions (cannot be
 used with \fB\-\-cover\fR)
 .PP
@@ -108,9 +108,8 @@ disable signed arithmetic over\- and underflow checks
 \fB\-\-no\-malloc\-may\-fail\fR
 do not allow malloc calls to fail by default
 .TP
-\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
-do not generate unwinding assertions (cannot be
-used with \fB\-\-cover\fR)
+\fB\-\-no\-unwinding\-assertions\fR
+do not generate unwinding assertions
 .PP
 If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
 when default checks are already on, the flag is simply ignored.

doc/man/goto-instrument.1

@@ -862,8 +862,12 @@ read unwindset from file
 \fB\-\-partial\-loops\fR
 permit paths with partial loops
 .TP
+\fB\-\-no\-unwinding\-assertions\fR
+do not generate unwinding assertions
+.TP
 \fB\-\-unwinding\-assertions\fR
-generate unwinding assertions
+generate unwinding assertions (enabled by default; overrides
+\fB\-\-no\-unwinding\-assertions\fR when both of these are given)
 .TP
 \fB\-\-continue\-as\-loops\fR
 add loop for remaining iterations after unwound part

regression/goto-instrument/slice01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-may-fail --unwind 2 --full-slice --add-library _ --no-standard-checks
+--no-malloc-may-fail --unwind 2 --no-unwinding-assertions --full-slice --add-library _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice08/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---full-slice --unwind 1
+--full-slice --unwind 1 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice16/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---full-slice --unwind 2
+--full-slice --unwind 2 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/unwind-assume2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 9
+--unwind 9 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -201,9 +201,11 @@ int goto_instrument_parse_optionst::doit()
             ui_message_handler);
         }
 
-        bool unwinding_assertions=cmdline.isset("unwinding-assertions");
-        bool partial_loops=cmdline.isset("partial-loops");
         bool continue_as_loops=cmdline.isset("continue-as-loops");
+        bool partial_loops = cmdline.isset("partial-loops");
+        bool unwinding_assertions = cmdline.isset("unwinding-assertions") ||
+                                    (!continue_as_loops && !partial_loops &&
+                                     !cmdline.isset("no-unwinding-assertions"));
         if(continue_as_loops)
         {
           if(unwinding_assertions)
@@ -1996,7 +1998,9 @@ void goto_instrument_parse_optionst::help()
     HELP_UNWINDSET
     " {y--unwindset-file_<file>} \t read unwindset from file\n"
     " {y--partial-loops} \t permit paths with partial loops\n"
-    " {y--unwinding-assertions} \t generate unwinding assertions\n"
+    " {y--unwinding-assertions} \t generate unwinding assertions"
+    " (enabled by default)\n"
+    " {y--no-unwinding-assertions} \t do not generate unwinding assertions\n"
     " {y--continue-as-loops} \t add loop for remaining iterations after"
     " unwound part\n"
     " {y--k-induction} {uk} \t check loops with k-induction\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -60,6 +60,7 @@ Author: Daniel Kroening, kroening@kroening.com
   OPT_UNWINDSET \
   "(unwindset-file):" \
   "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
+  "(no-unwinding-assertions)" \
   "(log):" \
   "(call-graph)(reachable-call-graph)" \
   OPT_INSERT_FINAL_ASSERT_FALSE \