Abort after failing C assert

The C standard specifies behaviour of the "assert" macro as resulting in
an abort when the condition does not evaluate to true. Implement this
behaviour by inserting assume(0) after assert(0).

Fixes: #5505

Author: tautschnig

regression/cbmc/Bool5/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 
-Generated 4 VCC\(s\), 0 remaining after simplification
+Generated [34] VCC\(s\), 0 remaining after simplification
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/r_w_ok1/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
-^\*\* 2 of 12 failed
+^\*\* [12] of 12 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-instrument/assert1/test.desc

@@ -5,4 +5,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^[[:space:]]*IF
+^[[:space:]]*if

src/goto-instrument/goto_program2code.cpp

@@ -192,11 +192,23 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
       return convert_decl(target, upper_bound, dest);
 
     case ASSERT:
+    {
       system_headers.insert("assert.h");
       dest.add(code_assertt(target->get_condition()));
       dest.statements().back().add_source_location().set_comment(
         target->source_location().get_comment());
+
+      goto_programt::const_targett next = target;
+      ++next;
+      CHECK_RETURN(next != goto_program.instructions.end());
+      if(
+        next != upper_bound && next->is_assume() &&
+        target->get_condition() == next->get_condition())
+      {
+        ++target;
+      }
       return target;
+    }
 
     case ASSUME:
       dest.add(code_assumet(target->guard));

src/goto-programs/builtin_functions.cpp

@@ -849,6 +849,12 @@ void goto_convertt::do_function_call_symbol(
       error() << identifier << " expected not to have LHS" << eom;
       throw 0;
     }
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
+      function.source_location()));
   }
   else if(identifier == CPROVER_PREFIX "enum_is_in_range")
   {
@@ -1092,6 +1098,11 @@ void goto_convertt::do_function_call_symbol(
     t->source_location_nonconst().set_property_class(ID_assertion);
     t->source_location_nonconst().set_comment(description);
     // we ignore any LHS
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      false_exprt(), function.source_location()));
   }
   else if(identifier=="__assert_rtn" ||
           identifier=="__assert")
@@ -1130,6 +1141,11 @@ void goto_convertt::do_function_call_symbol(
     t->source_location_nonconst().set_property_class(ID_assertion);
     t->source_location_nonconst().set_comment(description);
     // we ignore any LHS
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      false_exprt(), function.source_location()));
   }
   else if(identifier=="__assert_func")
   {
@@ -1164,6 +1180,11 @@ void goto_convertt::do_function_call_symbol(
     t->source_location_nonconst().set_property_class(ID_assertion);
     t->source_location_nonconst().set_comment(description);
     // we ignore any LHS
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      false_exprt(), function.source_location()));
   }
   else if(identifier==CPROVER_PREFIX "fence")
   {