Abort after failing C assert

regression/cbmc-cover/simple_assert/main.c

@@ -1,9 +1,7 @@
-#include <assert.h>
-
 int main(int argc, char *argv[])
 {
   int x = 5;
-  assert(x == 5);
+  __CPROVER_assert(x == 5, "assertion x == 5");
 
   return 0;
 }

regression/cbmc-cover/simple_assert/test.desc

@@ -9,5 +9,3 @@ main.c
 ^warning: ignoring
 ^CONVERSION ERROR$
 ^\[main\.coverage\..\] .* function main block .*: FAILED$
---
-On Windows/Visual Studio, "assert" does not introduce any branching.

regression/cbmc-incr-oneloop/multiple-asserts/test.c

@@ -2,8 +2,8 @@ int main()
 {
   for(int i = 0; i < 10; ++i)
   {
-    assert(i != 5);
-    assert(i != 8);
+    __CPROVER_assert(i != 5, "assertion i != 5");
+    __CPROVER_assert(i != 8, "assertion i != 8");
   }
   return 0;
 }

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/Quantifiers-not-exists/fixed.c

@@ -10,33 +10,43 @@ int main()
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && a[i][j]<=10}) });
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) && b[i][j]>=1 && b[i][j]<=10}) });
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (!__CPROVER_exists{int j; (j>=0 && j<2) && (c[i][j]==0 || c[i][j]<=10)}) });
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_forall{int j; (j>=0 && j<2) ==> d[i][j]>=1 && d[i][j]<=10}) });
   // clang-format on
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
-  assert(a[0][0] > 10);
+  __CPROVER_assert(a[0][0] > 10, "assertion a[0][0] > 10");
 
-  assert((b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10));
-  assert((b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10));
+  __CPROVER_assert(
+    (b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10),
+    "assertion (b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10)");
+  __CPROVER_assert(
+    (b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10),
+    "assertion (b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)");
 
-  assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10);
+  __CPROVER_assert(
+    c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10,
+    "assertion (b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)");
 
-  assert(((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)));
-  assert(((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)));
+  __CPROVER_assert(
+    (d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10),
+    "assertion (d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)");
+  __CPROVER_assert(
+    (d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10),
+    "assertion (d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)");
 
   return 0;
 }

regression/cbmc/Quantifiers-not-exists/fixed.desc

@@ -2,12 +2,12 @@ CORE broken-z3-smt-backend
 fixed.c
 
 ^\*\* Results:$
-^\[main.assertion.5\] line 31 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.6\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.7\] line 34 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.8\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.9\] line 38 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.10\] line 39 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.5\] line 31 assertion a\[0\]\[0\] > 10: SUCCESS$
+^\[main.assertion.6\] line 33 .*: SUCCESS$
+^\[main.assertion.7\] line 36 .*: SUCCESS$
+^\[main.assertion.8\] line 40 .*: SUCCESS$
+^\[main.assertion.9\] line 44 .*: SUCCESS$
+^\[main.assertion.10\] line 47 .*: SUCCESS$
 ^\*\* 4 of 10 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/double_deref/double_deref.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -12,5 +10,5 @@ int main(int argc, char **argv)
 
   pptr = (argc == 5 ? &ptr1 : &ptr2);
 
-  assert(**pptr == argc);
+  __CPROVER_assert(**pptr == argc, "assertion **pptr == argc");
 }

regression/cbmc/double_deref/double_deref_single_alias.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -10,5 +8,5 @@ int main(int argc, char **argv)
 
   pptr = &ptr1;
 
-  assert(**pptr == argc);
+  __CPROVER_assert(**pptr == argc, "assertion **pptr == argc");
 }

regression/cbmc/double_deref/double_deref_with_cast.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -12,5 +10,5 @@ int main(int argc, char **argv)
 
   pptr = (argc == 1 ? &ptr1 : &ptr2);
 
-  assert(*(int *)*pptr == argc);
+  __CPROVER_assert(*(int *)*pptr == argc, "assertion *(int *)*pptr == argc");
 }

regression/cbmc/double_deref/double_deref_with_cast_single_alias.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -10,5 +8,5 @@ int main(int argc, char **argv)
 
   pptr = &ptr1;
 
-  assert(*(int *)*pptr == argc);
+  __CPROVER_assert(*(int *)*pptr == argc, "assertion *(int *)*pptr == argc");
 }

regression/cbmc/double_deref/double_deref_with_member.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -18,5 +16,5 @@ int main(int argc, char **argv)
 
   cptr = (argc == 1 ? &container1 : &container2);
 
-  assert(*(cptr->iptr) == argc);
+  __CPROVER_assert(*(cptr->iptr) == argc, "assertion *(cptr->iptr) == argc");
 }

regression/cbmc/double_deref/double_deref_with_member_single_alias.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -16,5 +14,5 @@ int main(int argc, char **argv)
 
   cptr = &container1;
 
-  assert(*(cptr->iptr) == argc);
+  __CPROVER_assert(*(cptr->iptr) == argc, "assertion *(cptr->iptr) == argc");
 }

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -18,5 +16,6 @@ int main(int argc, char **argv)
   new_ptrs[argc % 2] = iptr1;
   new_ptrs[1 - (argc % 2)] = iptr2;
 
-  assert(*(new_ptrs[argc % 2]) == argc);
+  __CPROVER_assert(
+    *(new_ptrs[argc % 2]) == argc, "assertion *(new_ptrs[argc % 2]) == argc");
 }

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c

@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -15,5 +13,6 @@ int main(int argc, char **argv)
 
   new_ptrs[argc % 2] = iptr1;
 
-  assert(*(new_ptrs[argc % 2]) == argc);
+  __CPROVER_assert(
+    *(new_ptrs[argc % 2]) == argc, "assertion *(new_ptrs[argc % 2]) == argc");
 }

regression/cbmc/json-interface1/main.c

@@ -1,12 +1,10 @@
-#include <assert.h>
-
 void foo(int x)
 {
   for(int i = 0; i < 5; ++i)
   {
     if(x)
-      assert(0);
-    assert(0);
+      __CPROVER_assert(0, "assertion 0");
+    __CPROVER_assert(0, "assertion 0");
   }
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 }

regression/cbmc/json-interface1/test.desc

@@ -4,7 +4,7 @@ CORE
 activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
-Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
 \{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
 \{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
 VERIFICATION FAILED

regression/cbmc/multiple-goto-traces/main.c

@@ -1,14 +1,12 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
-  assert(4 != argc);
+  __CPROVER_assert(4 != argc, "assertion 4 != argc");
   argc++;
   argc--;
-  assert(argc >= 0);
-  assert(argc != 4);
+  __CPROVER_assert(argc >= 0, "assertion argc >= 0");
+  __CPROVER_assert(argc != 4, "assertion argc != 4");
   argc++;
   argc--;
-  assert(argc + 1 != 5);
+  __CPROVER_assert(argc + 1 != 5, "assertion argc + 1 != 5");
   return 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/cbmc/r_w_ok5/main.c

@@ -1,17 +1,16 @@
-#include <assert.h>
 #include <stdlib.h>
 
 void main()
 {
   char c[2];
-  assert(__CPROVER_r_ok(c, 2));
-  assert(!__CPROVER_r_ok(c, 2));
-  assert(__CPROVER_r_ok(c, 3));
-  assert(!__CPROVER_r_ok(c, 3));
+  __CPROVER_assert(__CPROVER_r_ok(c, 2), "assertion __CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(!__CPROVER_r_ok(c, 2), "assertion !__CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(__CPROVER_r_ok(c, 3), "assertion __CPROVER_r_ok(c, 3)");
+  __CPROVER_assert(!__CPROVER_r_ok(c, 3), "assertion !__CPROVER_r_ok(c, 3)");
 
   char *p = malloc(2);
-  assert(__CPROVER_r_ok(c, 2));
-  assert(!__CPROVER_r_ok(c, 2));
-  assert(__CPROVER_r_ok(p, 3));
-  assert(!__CPROVER_r_ok(p, 3));
+  __CPROVER_assert(__CPROVER_r_ok(c, 2), "assertion __CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(!__CPROVER_r_ok(c, 2), "assertion !__CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(__CPROVER_r_ok(p, 3), "assertion __CPROVER_r_ok(p, 3)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 3), "assertion !__CPROVER_r_ok(p, 3)");
 }

regression/cbmc/r_w_ok6/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 #include <stdlib.h>
 
 void main()
@@ -15,12 +14,12 @@ void main()
     p = malloc(3);
   }
 
-  assert(__CPROVER_r_ok(p, 2));
-  assert(!__CPROVER_r_ok(p, 2));
+  __CPROVER_assert(__CPROVER_r_ok(p, 2), "assertion __CPROVER_r_ok(p, 2)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 2), "assertion !__CPROVER_r_ok(p, 2)");
 
-  assert(__CPROVER_r_ok(p, 3));
-  assert(!__CPROVER_r_ok(p, 3));
+  __CPROVER_assert(__CPROVER_r_ok(p, 3), "assertion __CPROVER_r_ok(p, 3)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 3), "assertion !__CPROVER_r_ok(p, 3)");
 
-  assert(__CPROVER_r_ok(p, 4));
-  assert(!__CPROVER_r_ok(p, 4));
+  __CPROVER_assert(__CPROVER_r_ok(p, 4), "assertion __CPROVER_r_ok(p, 4)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 4), "assertion !__CPROVER_r_ok(p, 4)");
 }

regression/cbmc/reachability-slice-interproc/test.c

@@ -1,5 +1,3 @@
-#include <assert.h>
-
 // After a reachability slice based on the assertion in `target`, we should
 // retain both its possible callers (...may_call_target_1, ...may_call_target_2)
 // and their callees, but should be more precise concerning before_target and
@@ -22,7 +20,7 @@ void target()
   const char *local = "target_kept";
 
   before_target();
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
   after_target();
 }
 

regression/cbmc/xml-interface1/main.c

@@ -1,12 +1,10 @@
-#include <assert.h>
-
 void foo(int x)
 {
   for(int i = 0; i < 5; ++i)
   {
     if(x)
-      assert(0);
-    assert(0);
+      __CPROVER_assert(0, "assertion 0");
+    __CPROVER_assert(0, "assertion 0");
   }
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 }

regression/cbmc/xml-interface1/test.desc

@@ -3,7 +3,7 @@ CORE
 < test.xml
 ^EXIT=10$
 ^SIGNAL=0$
-Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
 <result property="foo\.assertion\.3" status="SUCCESS"/>
 <result property="foo\.assertion\.1" status="FAILURE">
 <goto_trace>

regression/goto-analyzer/command_line_01/main.c

@@ -1,16 +1,14 @@
-#include <assert.h>
-
 int f00(int x)
 {
-  assert(x != 0);
+  __CPROVER_assert(x != 0, "assertion x != 0");
   return 0;
 }
 
 int main(int argc, char **argv)
 {
   int v = 0;
   v = f00(v);
-  assert(v != 0);
+  __CPROVER_assert(v != 0, "assertion v != 0");
 
   return 0;
 }

regression/goto-analyzer/command_line_01/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 --verify --recursive-interprocedural --ahistorical --constants --one-domain-per-history
-\[main.assertion.1\] line 13 assertion v != 0: FAILURE \(if reachable\)
-\[f00.assertion.1\] line 5 assertion x != 0: FAILURE \(if reachable\)
+\[main.assertion.1\] line 11 assertion v != 0: FAILURE \(if reachable\)
+\[f00.assertion.1\] line 3 assertion x != 0: FAILURE \(if reachable\)
 Summary: 0 pass, 2 fail if reachable, 0 unknown
 ^EXIT=0$
 ^SIGNAL=0$