Built-in checks can optionally be fatal

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],

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

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],

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

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");
+}

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$
+--

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");
+}

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$
+--

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));
         }
       }
     }

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"));      \