Skip to content

Commit 60c388e

Browse files
tautschnigtautschnig
committed
Regression tests: use __CPROVER_assert when multiple properties may fail
C's assert() should result in an abort() when the asserted condition evaluates to false. If we want to test multiple properties, including some failing ones, use __CPROVER_assert to not rely on any modelling of assert() that does not result in an abort().
1 parent c41ce2b commit 60c388e

File tree

84 files changed

+326
-339
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

84 files changed

+326
-339
lines changed

‎regression/cbmc-cover/simple_assert/main.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
1-
#include <assert.h>
2-
31
int main(int argc, char *argv[])
42
{
53
int x = 5;
6-
assert(x == 5);
4+
__CPROVER_assert(x == 5, "assertion x == 5");
75

86
return 0;
97
}

‎regression/cbmc-cover/simple_assert/test.desc

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,3 @@ main.c
99
^warning: ignoring
1010
^CONVERSION ERROR$
1111
^\[main\.coverage\..\] .* function main block .*: FAILED$
12-
--
13-
On Windows/Visual Studio, "assert" does not introduce any branching.

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

‎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, "assertion 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, "assertion 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, "assertion 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, "assertion 0");
3030

31-
assert(a[0][0] > 10);
31+
__CPROVER_assert(a[0][0] > 10, "assertion 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+
"assertion (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+
"assertion (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+
"assertion (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+
"assertion (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+
"assertion (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 assertion 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, "assertion **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, "assertion **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, "assertion *(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, "assertion *(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, "assertion *(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, "assertion *(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, "assertion *(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, "assertion *(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, "assertion 0");
7+
__CPROVER_assert(0, "assertion 0");
108
}
11-
assert(0);
9+
__CPROVER_assert(0, "assertion 0");
1210
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ 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
7+
Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
88
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
99
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
1010
VERIFICATION FAILED

‎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, "assertion 4 != argc");
64
argc++;
75
argc--;
8-
assert(argc >= 1);
9-
assert(argc != 4);
6+
__CPROVER_assert(argc >= 1, "assertion argc >= 1");
7+
__CPROVER_assert(argc != 4, "assertion argc != 4");
108
argc++;
119
argc--;
12-
assert(argc + 1 != 5);
10+
__CPROVER_assert(argc + 1 != 5, "assertion argc + 1 != 5");
1311
return 0;
1412
}

‎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), "assertion __CPROVER_r_ok(c, 2)");
7+
__CPROVER_assert(!__CPROVER_r_ok(c, 2), "assertion !__CPROVER_r_ok(c, 2)");
8+
__CPROVER_assert(__CPROVER_r_ok(c, 3), "assertion __CPROVER_r_ok(c, 3)");
9+
__CPROVER_assert(!__CPROVER_r_ok(c, 3), "assertion !__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), "assertion __CPROVER_r_ok(c, 2)");
13+
__CPROVER_assert(!__CPROVER_r_ok(c, 2), "assertion !__CPROVER_r_ok(c, 2)");
14+
__CPROVER_assert(__CPROVER_r_ok(p, 3), "assertion __CPROVER_r_ok(p, 3)");
15+
__CPROVER_assert(!__CPROVER_r_ok(p, 3), "assertion !__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), "assertion __CPROVER_r_ok(p, 2)");
18+
__CPROVER_assert(!__CPROVER_r_ok(p, 2), "assertion !__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), "assertion __CPROVER_r_ok(p, 3)");
21+
__CPROVER_assert(!__CPROVER_r_ok(p, 3), "assertion !__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), "assertion __CPROVER_r_ok(p, 4)");
24+
__CPROVER_assert(!__CPROVER_r_ok(p, 4), "assertion !__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, "assertion 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, "assertion 0");
7+
__CPROVER_assert(0, "assertion 0");
108
}
11-
assert(0);
9+
__CPROVER_assert(0, "assertion 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-analyzer/command_line_01/main.c

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,14 @@
1-
#include <assert.h>
2-
31
int f00(int x)
42
{
5-
assert(x != 0);
3+
__CPROVER_assert(x != 0, "assertion x != 0");
64
return 0;
75
}
86

97
int main(int argc, char **argv)
108
{
119
int v = 0;
1210
v = f00(v);
13-
assert(v != 0);
11+
__CPROVER_assert(v != 0, "assertion v != 0");
1412

1513
return 0;
1614
}

‎regression/goto-analyzer/command_line_01/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--verify --recursive-interprocedural --ahistorical --constants --one-domain-per-history
4-
\[main.assertion.1\] line 13 assertion v != 0: FAILURE \(if reachable\)
5-
\[f00.assertion.1\] line 5 assertion x != 0: FAILURE \(if reachable\)
4+
\[main.assertion.1\] line 11 assertion v != 0: FAILURE \(if reachable\)
5+
\[f00.assertion.1\] line 3 assertion x != 0: FAILURE \(if reachable\)
66
Summary: 0 pass, 2 fail if reachable, 0 unknown
77
^EXIT=0$
88
^SIGNAL=0$

‎regression/goto-analyzer/command_line_02/main.c

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,14 @@
1-
#include <assert.h>
2-
31
int f00(int x)
42
{
5-
assert(x != 0);
3+
__CPROVER_assert(x != 0, "assertion x != 0");
64
return 0;
75
}
86

97
int main(int argc, char **argv)
108
{
119
int v = 0;
1210
v = f00(v);
13-
assert(v != 0);
11+
__CPROVER_assert(v != 0, "assertion v != 0");
1412

1513
return 0;
1614
}

0 commit comments

Comments
 (0)