Skip to content

Commit f75988e

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 99741b3 commit f75988e

File tree

6 files changed

+54
-28
lines changed

6 files changed

+54
-28
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, "");
6+
__CPROVER_assert(i != 8, "");
77
}
88
return 0;
99
}

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

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,33 +10,38 @@ 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, "");
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, "");
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, "");
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, "");
3030

31-
assert(a[0][0] > 10);
31+
__CPROVER_assert(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+
__CPROVER_assert(
36+
(b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10), "");
3537

36-
assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10);
38+
__CPROVER_assert(
39+
c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10, "");
3740

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)));
41+
__CPROVER_assert(
42+
((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)), "");
43+
__CPROVER_assert(
44+
((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)), "");
4045

4146
return 0;
4247
}

‎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 assertion: SUCCESS$
6+
^\[main.assertion.6\] line 33 assertion: SUCCESS$
7+
^\[main.assertion.7\] line 35 assertion: SUCCESS$
8+
^\[main.assertion.8\] line 38 assertion: SUCCESS$
9+
^\[main.assertion.9\] line 41 assertion: SUCCESS$
10+
^\[main.assertion.10\] line 43 assertion: SUCCESS$
1111
^\*\* 4 of 10 failed
1212
^VERIFICATION FAILED$
1313
^EXIT=10$

‎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, "");
4+
__CPROVER_assert(y, "");
5+
__CPROVER_assert(x == y, "");
6+
__CPROVER_assert(x != y, "");
7+
__CPROVER_assert(*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 assertion: SUCCESS
6+
\[test.assertion.2\] line 4 assertion: SUCCESS
7+
\[test.assertion.3\] line 5 assertion: FAILURE
8+
\[test.assertion.4\] line 6 assertion: FAILURE
9+
\[test.assertion.5\] line 7 assertion: FAILURE
1010
^EXIT=10$
1111
^SIGNAL=0$
1212
--

‎src/goto-programs/builtin_functions.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -760,6 +760,12 @@ void goto_convertt::do_function_call_symbol(
760760
error() << identifier << " expected not to have LHS" << eom;
761761
throw 0;
762762
}
763+
764+
// The C standard mandates that a failing assertion causes execution to
765+
// abort:
766+
dest.add(goto_programt::make_assumption(
767+
typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
768+
function.source_location()));
763769
}
764770
else if(identifier == CPROVER_PREFIX "enum_is_in_range")
765771
{
@@ -1004,6 +1010,11 @@ void goto_convertt::do_function_call_symbol(
10041010
t->source_location.set_property_class(ID_assertion);
10051011
t->source_location.set_comment(description);
10061012
// we ignore any LHS
1013+
1014+
// The C standard mandates that a failing assertion causes execution to
1015+
// abort:
1016+
dest.add(goto_programt::make_assumption(
1017+
false_exprt(), function.source_location()));
10071018
}
10081019
else if(identifier=="__assert_rtn" ||
10091020
identifier=="__assert")
@@ -1042,6 +1053,11 @@ void goto_convertt::do_function_call_symbol(
10421053
t->source_location.set_property_class(ID_assertion);
10431054
t->source_location.set_comment(description);
10441055
// we ignore any LHS
1056+
1057+
// The C standard mandates that a failing assertion causes execution to
1058+
// abort:
1059+
dest.add(goto_programt::make_assumption(
1060+
false_exprt(), function.source_location()));
10451061
}
10461062
else if(identifier=="__assert_func")
10471063
{
@@ -1076,6 +1092,11 @@ void goto_convertt::do_function_call_symbol(
10761092
t->source_location.set_property_class(ID_assertion);
10771093
t->source_location.set_comment(description);
10781094
// we ignore any LHS
1095+
1096+
// The C standard mandates that a failing assertion causes execution to
1097+
// abort:
1098+
dest.add(goto_programt::make_assumption(
1099+
false_exprt(), function.source_location()));
10791100
}
10801101
else if(identifier==CPROVER_PREFIX "fence")
10811102
{

0 commit comments

Comments
 (0)