Skip to content

Commit 9b215f7

Browse files
tautschnigtautschnig
committed
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).
1 parent 87ef739 commit 9b215f7

File tree

25 files changed

+101
-94
lines changed

25 files changed

+101
-94
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ int main()
22
{
33
for(int i = 0; i < 10; ++i)
44
{
5-
assert(i != 5);
6-
assert(i != 8);
5+
__CPROVER_assert(i != 5, "i != 5");
6+
__CPROVER_assert(i != 8, "i != 8");
77
}
88
return 0;
99
}

‎regression/cbmc/Bool5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33

4-
Generated 4 VCC\(s\), 0 remaining after simplification
4+
Generated [34] VCC\(s\), 0 remaining after simplification
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$
77
^SIGNAL=0$

‎regression/cbmc/Quantifiers-not-exists/fixed.c

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,33 +10,43 @@ int main()
1010
// NOLINTNEXTLINE(whitespace/line_length)
1111
__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && a[i][j]<=10}) });
1212

13-
assert(0);
13+
__CPROVER_assert(0, "0");
1414

1515
// NOLINTNEXTLINE(whitespace/line_length)
1616
__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}) });
1717

18-
assert(0);
18+
__CPROVER_assert(0, "0");
1919

2020
// NOLINTNEXTLINE(whitespace/line_length)
2121
__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)}) });
2222

23-
assert(0);
23+
__CPROVER_assert(0, "0");
2424

2525
// NOLINTNEXTLINE(whitespace/line_length)
2626
__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}) });
2727
// clang-format on
2828

29-
assert(0);
29+
__CPROVER_assert(0, "0");
3030

31-
assert(a[0][0] > 10);
31+
__CPROVER_assert(a[0][0] > 10, "a[0][0] > 10");
3232

33-
assert((b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10));
34-
assert((b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10));
33+
__CPROVER_assert(
34+
(b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10),
35+
"(b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10)");
36+
__CPROVER_assert(
37+
(b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10),
38+
"(b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)");
3539

36-
assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10);
40+
__CPROVER_assert(
41+
c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10,
42+
"(b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)");
3743

38-
assert(((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)));
39-
assert(((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)));
44+
__CPROVER_assert(
45+
((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)),
46+
"((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10))");
47+
__CPROVER_assert(
48+
((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)),
49+
"((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10))");
4050

4151
return 0;
4252
}

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ CORE
22
fixed.c
33

44
^\*\* Results:$
5-
^\[main.assertion.5\] line 31 assertion a\[.*\]\[.*\] > 10: SUCCESS$
6-
^\[main.assertion.6\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
7-
^\[main.assertion.7\] line 34 assertion tmp_if_expr\$\d+: SUCCESS$
8-
^\[main.assertion.8\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
9-
^\[main.assertion.9\] line 38 assertion tmp_if_expr\$\d+: SUCCESS$
10-
^\[main.assertion.10\] line 39 assertion tmp_if_expr\$\d+: SUCCESS$
5+
^\[main.assertion.5\] line 31 a\[0\]\[0\] > 10: SUCCESS$
6+
^\[main.assertion.6\] line 33 .*: SUCCESS$
7+
^\[main.assertion.7\] line 36 .*: SUCCESS$
8+
^\[main.assertion.8\] line 40 .*: SUCCESS$
9+
^\[main.assertion.9\] line 44 .*: SUCCESS$
10+
^\[main.assertion.10\] line 47 .*: SUCCESS$
1111
^\*\* 4 of 10 failed
1212
^VERIFICATION FAILED$
1313
^EXIT=10$

‎regression/cbmc/double_deref/double_deref.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
int main(int argc, char **argv)
@@ -12,5 +10,5 @@ int main(int argc, char **argv)
1210

1311
pptr = (argc == 5 ? &ptr1 : &ptr2);
1412

15-
assert(**pptr == argc);
13+
__CPROVER_assert(**pptr == argc, "**pptr == argc");
1614
}

‎regression/cbmc/double_deref/double_deref_single_alias.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
int main(int argc, char **argv)
@@ -10,5 +8,5 @@ int main(int argc, char **argv)
108

119
pptr = &ptr1;
1210

13-
assert(**pptr == argc);
11+
__CPROVER_assert(**pptr == argc, "**pptr == argc");
1412
}

‎regression/cbmc/double_deref/double_deref_with_cast.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
int main(int argc, char **argv)
@@ -12,5 +10,5 @@ int main(int argc, char **argv)
1210

1311
pptr = (argc == 1 ? &ptr1 : &ptr2);
1412

15-
assert(*(int *)*pptr == argc);
13+
__CPROVER_assert(*(int *)*pptr == argc, "*(int *)*pptr == argc");
1614
}

‎regression/cbmc/double_deref/double_deref_with_cast_single_alias.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
int main(int argc, char **argv)
@@ -10,5 +8,5 @@ int main(int argc, char **argv)
108

119
pptr = &ptr1;
1210

13-
assert(*(int *)*pptr == argc);
11+
__CPROVER_assert(*(int *)*pptr == argc, "*(int *)*pptr == argc");
1412
}

‎regression/cbmc/double_deref/double_deref_with_member.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
struct container
@@ -18,5 +16,5 @@ int main(int argc, char **argv)
1816

1917
cptr = (argc == 1 ? &container1 : &container2);
2018

21-
assert(*(cptr->iptr) == argc);
19+
__CPROVER_assert(*(cptr->iptr) == argc, "*(cptr->iptr) == argc");
2220
}

‎regression/cbmc/double_deref/double_deref_with_member_single_alias.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
struct container
@@ -16,5 +14,5 @@ int main(int argc, char **argv)
1614

1715
cptr = &container1;
1816

19-
assert(*(cptr->iptr) == argc);
17+
__CPROVER_assert(*(cptr->iptr) == argc, "*(cptr->iptr) == argc");
2018
}

‎regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
struct container
@@ -18,5 +16,6 @@ int main(int argc, char **argv)
1816
new_ptrs[argc % 2] = iptr1;
1917
new_ptrs[1 - (argc % 2)] = iptr2;
2018

21-
assert(*(new_ptrs[argc % 2]) == argc);
19+
__CPROVER_assert(
20+
*(new_ptrs[argc % 2]) == argc, "*(new_ptrs[argc % 2]) == argc");
2221
}

‎regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
2-
#include <assert.h>
31
#include <stdlib.h>
42

53
struct container
@@ -15,5 +13,6 @@ int main(int argc, char **argv)
1513

1614
new_ptrs[argc % 2] = iptr1;
1715

18-
assert(*(new_ptrs[argc % 2]) == argc);
16+
__CPROVER_assert(
17+
*(new_ptrs[argc % 2]) == argc, "*(new_ptrs[argc % 2]) == argc");
1918
}

‎regression/cbmc/json-interface1/main.c

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,10 @@
1-
#include <assert.h>
2-
31
void foo(int x)
42
{
53
for(int i = 0; i < 5; ++i)
64
{
75
if(x)
8-
assert(0);
9-
assert(0);
6+
__CPROVER_assert(0, "0");
7+
__CPROVER_assert(0, "0");
108
}
11-
assert(0);
9+
__CPROVER_assert(0, "0");
1210
}

‎regression/cbmc/json-interface1/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ CORE broken-smt-backend
44
activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
7-
Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
8-
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
9-
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
7+
Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
8+
\{\n\s*"description": "0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
9+
\{\n\s*"description": "0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
1010
VERIFICATION FAILED
1111
--
1212
"property": "foo\.assertion\.2"

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

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,12 @@
1-
#include <assert.h>
2-
31
int main(int argc, char **argv)
42
{
5-
assert(4 != argc);
3+
__CPROVER_assert(4 != argc, "4 != argc");
64
argc++;
75
argc--;
8-
assert(argc >= 1);
9-
assert(argc != 4);
6+
__CPROVER_assert(argc >= 1, "argc >= 1");
7+
__CPROVER_assert(argc != 4, "argc != 4");
108
argc++;
119
argc--;
12-
assert(argc + 1 != 5);
10+
__CPROVER_assert(argc + 1 != 5, "argc + 1 != 5");
1311
return 0;
1412
}

‎regression/cbmc/multiple-goto-traces/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
77
VERIFICATION FAILED
8-
Trace for main\.assertion\.1:(\n.*){22} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50} assertion argc \+ 1 != 5
8+
Trace for main\.assertion\.1:(\n.*){22} 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36} argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50} argc \+ 1 != 5
99
\*\* 3 of 4 failed
1010
--
1111
^warning: ignoring

‎regression/cbmc/r_w_ok1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33

44
__CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
5-
^\*\* 2 of 12 failed
5+
^\*\* [12] of 12 failed
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/cbmc/r_w_ok5/main.c

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,16 @@
1-
#include <assert.h>
21
#include <stdlib.h>
32

43
void main()
54
{
65
char c[2];
7-
assert(__CPROVER_r_ok(c, 2));
8-
assert(!__CPROVER_r_ok(c, 2));
9-
assert(__CPROVER_r_ok(c, 3));
10-
assert(!__CPROVER_r_ok(c, 3));
6+
__CPROVER_assert(__CPROVER_r_ok(c, 2), "__CPROVER_r_ok(c, 2)");
7+
__CPROVER_assert(!__CPROVER_r_ok(c, 2), "!__CPROVER_r_ok(c, 2)");
8+
__CPROVER_assert(__CPROVER_r_ok(c, 3), "__CPROVER_r_ok(c, 3)");
9+
__CPROVER_assert(!__CPROVER_r_ok(c, 3), "!__CPROVER_r_ok(c, 3)");
1110

1211
char *p = malloc(2);
13-
assert(__CPROVER_r_ok(c, 2));
14-
assert(!__CPROVER_r_ok(c, 2));
15-
assert(__CPROVER_r_ok(p, 3));
16-
assert(!__CPROVER_r_ok(p, 3));
12+
__CPROVER_assert(__CPROVER_r_ok(c, 2), "__CPROVER_r_ok(c, 2)");
13+
__CPROVER_assert(!__CPROVER_r_ok(c, 2), "!__CPROVER_r_ok(c, 2)");
14+
__CPROVER_assert(__CPROVER_r_ok(p, 3), "__CPROVER_r_ok(p, 3)");
15+
__CPROVER_assert(!__CPROVER_r_ok(p, 3), "!__CPROVER_r_ok(p, 3)");
1716
}

‎regression/cbmc/r_w_ok6/main.c

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21
#include <stdlib.h>
32

43
void main()
@@ -15,12 +14,12 @@ void main()
1514
p = malloc(3);
1615
}
1716

18-
assert(__CPROVER_r_ok(p, 2));
19-
assert(!__CPROVER_r_ok(p, 2));
17+
__CPROVER_assert(__CPROVER_r_ok(p, 2), "__CPROVER_r_ok(p, 2)");
18+
__CPROVER_assert(!__CPROVER_r_ok(p, 2), "!__CPROVER_r_ok(p, 2)");
2019

21-
assert(__CPROVER_r_ok(p, 3));
22-
assert(!__CPROVER_r_ok(p, 3));
20+
__CPROVER_assert(__CPROVER_r_ok(p, 3), "__CPROVER_r_ok(p, 3)");
21+
__CPROVER_assert(!__CPROVER_r_ok(p, 3), "!__CPROVER_r_ok(p, 3)");
2322

24-
assert(__CPROVER_r_ok(p, 4));
25-
assert(!__CPROVER_r_ok(p, 4));
23+
__CPROVER_assert(__CPROVER_r_ok(p, 4), "__CPROVER_r_ok(p, 4)");
24+
__CPROVER_assert(!__CPROVER_r_ok(p, 4), "!__CPROVER_r_ok(p, 4)");
2625
}

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
// After a reachability slice based on the assertion in `target`, we should
42
// retain both its possible callers (...may_call_target_1, ...may_call_target_2)
53
// and their callees, but should be more precise concerning before_target and
@@ -22,7 +20,7 @@ void target()
2220
const char *local = "target_kept";
2321

2422
before_target();
25-
assert(0);
23+
__CPROVER_assert(0, "0");
2624
after_target();
2725
}
2826

‎regression/cbmc/xml-interface1/main.c

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,10 @@
1-
#include <assert.h>
2-
31
void foo(int x)
42
{
53
for(int i = 0; i < 5; ++i)
64
{
75
if(x)
8-
assert(0);
9-
assert(0);
6+
__CPROVER_assert(0, "0");
7+
__CPROVER_assert(0, "0");
108
}
11-
assert(0);
9+
__CPROVER_assert(0, "0");
1210
}

‎regression/cbmc/xml-interface1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ CORE
33
< test.xml
44
^EXIT=10$
55
^SIGNAL=0$
6-
Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
6+
Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
77
<result property="foo\.assertion\.3" status="SUCCESS"/>
88
<result property="foo\.assertion\.1" status="FAILURE">
99
<goto_trace>

‎regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
void test(int *x, int *y)
22
{
3-
assert(x);
4-
assert(y);
5-
assert(x == y);
6-
assert(x != y);
7-
assert(*x == *y);
3+
__CPROVER_assert(x, "x");
4+
__CPROVER_assert(y, "y");
5+
__CPROVER_assert(x == y, "x == y");
6+
__CPROVER_assert(x != y, "x != y");
7+
__CPROVER_assert(*x == *y, "*x == *y");
88
}

‎regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,11 @@ CORE
22
test.c
33
--function test --harness-type call-function --treat-pointers-equal x,y --treat-pointers-equal-maybe
44
should_make_equal
5-
\[test.assertion.1\] line 3 assertion x: SUCCESS
6-
\[test.assertion.2\] line 4 assertion y: SUCCESS
7-
\[test.assertion.3\] line 5 assertion x == y: FAILURE
8-
\[test.assertion.4\] line 6 assertion x != y: FAILURE
9-
\[test.assertion.5\] line 7 assertion \*x == \*y: FAILURE
5+
\[test.assertion.1\] line 3 x: SUCCESS
6+
\[test.assertion.2\] line 4 y: SUCCESS
7+
\[test.assertion.3\] line 5 x == y: FAILURE
8+
\[test.assertion.4\] line 6 x != y: FAILURE
9+
\[test.assertion.5\] line 7 \*x == \*y: FAILURE
1010
^EXIT=10$
1111
^SIGNAL=0$
1212
--

0 commit comments

Comments
 (0)