From 900acce2662f314a16ab4e20bf0e72584078386c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 3 May 2024 12:00:20 +0000 Subject: [PATCH] goto-instrument/unwinding: enable unwinding assertions by default This will make behaviour consistent (and sound-by-default) across CBMC and goto-instrument. --- doc/man/cbmc.1 | 7 +++---- doc/man/goto-instrument.1 | 6 +++++- regression/goto-instrument/slice01/test.desc | 2 +- regression/goto-instrument/slice08/test.desc | 2 +- regression/goto-instrument/slice16/test.desc | 2 +- regression/goto-instrument/unwind-assume2/test.desc | 2 +- src/goto-instrument/goto_instrument_parse_options.cpp | 10 +++++++--- src/goto-instrument/goto_instrument_parse_options.h | 1 + 8 files changed, 20 insertions(+), 12 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 6798f463eb9..7b8b8fcf243 100644 --- a/doc/man/cbmc.1 +++ b/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. diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 03141e2f55c..92342ceb482 100644 --- a/doc/man/goto-instrument.1 +++ b/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 diff --git a/regression/goto-instrument/slice01/test.desc b/regression/goto-instrument/slice01/test.desc index fb7edea5abc..8de6729aadd 100644 --- a/regression/goto-instrument/slice01/test.desc +++ b/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$ diff --git a/regression/goto-instrument/slice08/test.desc b/regression/goto-instrument/slice08/test.desc index 67625747cf1..110e722c03f 100644 --- a/regression/goto-instrument/slice08/test.desc +++ b/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$ diff --git a/regression/goto-instrument/slice16/test.desc b/regression/goto-instrument/slice16/test.desc index ab6fd2dd827..3ec0d3ddee6 100644 --- a/regression/goto-instrument/slice16/test.desc +++ b/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$ diff --git a/regression/goto-instrument/unwind-assume2/test.desc b/regression/goto-instrument/unwind-assume2/test.desc index d8bb57ee3c2..3309713949a 100644 --- a/regression/goto-instrument/unwind-assume2/test.desc +++ b/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$ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index b26f65efe26..c38bd5d846c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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_} \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" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5b64af490e5..7bb0b91d4ab 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/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 \