diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 581c859b7f8..a852b1f7832 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -304,6 +304,9 @@ ignore user assumptions \fB\-\-assert\-to\-assume\fR convert user assertions to assumptions .TP +\fB\-\-assert\-then\-assume\fR +follow each inserted check by an assumption +.TP \fB\-\-cover\fR CC create test\-suite with coverage criterion CC, where CC is one of assertion[s], assume[s], diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index 9517eef3072..6abcbe62a54 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -568,6 +568,9 @@ ignore user assumptions \fB\-\-assert\-to\-assume\fR convert user assertions to assumptions .TP +\fB\-\-assert\-then\-assume\fR +follow each inserted check by an assumption +.TP \fB\-\-malloc\-may\-fail\fR allow malloc calls to return a null pointer .TP diff --git a/doc/man/goto-diff.1 b/doc/man/goto-diff.1 index 5bb6318c6e4..c62bac4ba48 100644 --- a/doc/man/goto-diff.1 +++ b/doc/man/goto-diff.1 @@ -99,6 +99,9 @@ ignore user assumptions \fB\-\-assert\-to\-assume\fR convert user assertions to assumptions .TP +\fB\-\-assert\-then\-assume\fR +follow each inserted check by an assumption +.TP \fB\-\-cover\fR CC create test\-suite with coverage criterion CC, where CC is one of assertion[s], assume[s], diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 88428b58c7c..ad480583ae3 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -239,6 +239,9 @@ ignore user assumptions \fB\-\-assert\-to\-assume\fR convert user assertions to assumptions .TP +\fB\-\-assert\-then\-assume\fR +follow each inserted check by an assumption +.TP \fB\-\-uninitialized\-check\fR add checks for uninitialized locals (experimental) .TP diff --git a/regression/cbmc/assert-then-assume/main.c b/regression/cbmc/assert-then-assume/main.c new file mode 100644 index 00000000000..2a812236ce9 --- /dev/null +++ b/regression/cbmc/assert-then-assume/main.c @@ -0,0 +1,9 @@ +int nondet_int(); + +int main() +{ + int x; + int *p = nondet_int() ? (int *)0 : &x; + *p = 42; + __CPROVER_assert(x == 42, "cannot fail with assert-to-assume"); +} diff --git a/regression/cbmc/assert-then-assume/test.desc b/regression/cbmc/assert-then-assume/test.desc new file mode 100644 index 00000000000..9b45ecd3d93 --- /dev/null +++ b/regression/cbmc/assert-then-assume/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--assert-then-assume +^\[main.pointer_dereference.1\] line 7 dereference failure: pointer NULL in \*p: FAILURE$ +^\[main.assertion.1\] line 8 cannot fail with assert-to-assume: SUCCESS$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- diff --git a/regression/cbmc/assert-to-assume/main.c b/regression/cbmc/assert-to-assume/main.c new file mode 100644 index 00000000000..2a812236ce9 --- /dev/null +++ b/regression/cbmc/assert-to-assume/main.c @@ -0,0 +1,9 @@ +int nondet_int(); + +int main() +{ + int x; + int *p = nondet_int() ? (int *)0 : &x; + *p = 42; + __CPROVER_assert(x == 42, "cannot fail with assert-to-assume"); +} diff --git a/regression/cbmc/assert-to-assume/test.desc b/regression/cbmc/assert-to-assume/test.desc new file mode 100644 index 00000000000..d0d7525fe9a --- /dev/null +++ b/regression/cbmc/assert-to-assume/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--assert-to-assume +^\[main.assertion.1\] line 8 cannot fail with assert-to-assume: SUCCESS$ +^\*\* 0 of 1 failed +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 992d9af33e7..9f47ea90587 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -74,6 +74,7 @@ class goto_check_ct enable_nan_check = _options.get_bool_option("nan-check"); retain_trivial = _options.get_bool_option("retain-trivial-checks"); enable_assert_to_assume = _options.get_bool_option("assert-to-assume"); + enable_assert_then_assume = _options.get_bool_option("assert-then-assume"); error_labels = _options.get_list_option("error-label"); enable_pointer_primitive_check = _options.get_bool_option("pointer-primitive-check"); @@ -273,6 +274,7 @@ class goto_check_ct bool enable_nan_check; bool retain_trivial; bool enable_assert_to_assume; + bool enable_assert_then_assume; bool enable_pointer_primitive_check; /// Maps a named-check name to the corresponding boolean flag. @@ -1719,14 +1721,14 @@ void goto_check_ct::add_guarded_property( add_all_checked_named_check_pragmas(annotated_location); - if(enable_assert_to_assume) + if(!enable_assert_to_assume) { - new_code.add(goto_programt::make_assumption( + new_code.add(goto_programt::make_assertion( std::move(guarded_expr), annotated_location)); } - else + if(enable_assert_to_assume || enable_assert_then_assume) { - new_code.add(goto_programt::make_assertion( + new_code.add(goto_programt::make_assumption( std::move(guarded_expr), annotated_location)); } } @@ -2082,15 +2084,15 @@ void goto_check_ct::goto_check( annotated_location.set_comment("error label " + label); annotated_location.set("user-provided", true); - if(enable_assert_to_assume) + if(!enable_assert_to_assume) { new_code.add( - goto_programt::make_assumption(false_exprt{}, annotated_location)); + goto_programt::make_assertion(false_exprt{}, annotated_location)); } - else + if(enable_assert_to_assume || enable_assert_then_assume) { new_code.add( - goto_programt::make_assertion(false_exprt{}, annotated_location)); + goto_programt::make_assumption(false_exprt{}, annotated_location)); } } } diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 9fcf818241b..534b0805085 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -48,6 +48,7 @@ void goto_check_c( "(error-label):" \ "(no-assertions)(no-assumptions)" \ "(assert-to-assume)" \ + "(assert-then-assume)" \ "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)" \ "(no-pointer-primitive-check)(no-undefined-shift-check)" \ "(no-div-by-zero-check)" @@ -91,7 +92,8 @@ void goto_check_c( " {y--no-built-in-assertions} \t ignore assertions in built-in library\n" \ " {y--no-assertions} \t ignore user assertions\n" \ " {y--no-assumptions} \t ignore user assumptions\n" \ - " {y--assert-to-assume} \t convert user assertions to assumptions\n" + " {y--assert-to-assume} \t convert user assertions to assumptions\n" \ + " {y--assert-then-assume} \t follow each inserted check by an assumption\n" // clang-format on #define PARSE_OPTION_OVERRIDE(cmdline, options, option) \ @@ -117,6 +119,7 @@ void goto_check_c( options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \ options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \ options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("assert-then-assume", cmdline.isset("assert-then-assume")); /* NOLINT(whitespace/line_length) */ \ options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \ if(cmdline.isset("error-label")) \ options.set_option("error-label", cmdline.get_values("error-label")); \