goto-instrument/unwinding: enable unwinding assertions by default

This will make behaviour consistent (and sound-by-default) across CBMC
and goto-instrument.

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -201,7 +201,8 @@ int goto_instrument_parse_optionst::doit()
             ui_message_handler);
         }
 
-        bool unwinding_assertions=cmdline.isset("unwinding-assertions");
+        bool unwinding_assertions = cmdline.isset("unwinding-assertions") ||
+                                    !cmdline.isset("no-unwinding-assertions");
         bool partial_loops=cmdline.isset("partial-loops");
         bool continue_as_loops=cmdline.isset("continue-as-loops");
         if(continue_as_loops)
@@ -1996,7 +1997,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, [email protected]
   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 \