Skip to content

Commit 12c622d

Browse files
tautschnigtautschnig
authored
Merge pull request #3724 from tautschnig/fix-quant-test
Quantifier test: The second assertion does not hold [blocks: #2574, #3725, #3924]
2 parents d785393 + 52794ca commit 12c622d

File tree

28 files changed

+198
-25
lines changed

28 files changed

+198
-25
lines changed

‎regression/cbmc/Quantifiers-assertion/main.c

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,12 @@ int main()
77
c[1][0]=1;
88
c[1][1]=2;
99

10+
// clang-format off
11+
// clang-format would rewrite the "==>" as "== >"
1012
__CPROVER_assert(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "Exists-Exists: successful");
1113

12-
__CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-NotExists: successful");
14+
// NOLINTNEXTLINE(whitespace/line_length)
15+
__CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-NotExists: failed");
1316

1417
__CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-Exists: failed");
1518

@@ -18,6 +21,7 @@ int main()
1821
__CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-Forall: successful");
1922

2023
__CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-NotForall: successful");
24+
// clang-format on
2125

2226
return 0;
2327
}

‎regression/cbmc/Quantifiers-assertion/test.desc

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^\*\* Results:$
55
^\[main.assertion.1\] .* Exists-Exists: successful: SUCCESS$
6-
^\[main.assertion.2\] .* NotExists-NotExists: successful: SUCCESS$
6+
^\[main.assertion.2\] .* NotExists-NotExists: failed: FAILURE$
77
^\[main.assertion.3\] .* NotExists-Exists: failed: FAILURE$
88
^\[main.assertion.4\] .* NotExists-Forall: failed: FAILURE$
99
^\[main.assertion.5\] .* NotForall-Forall: successful: SUCCESS$
1010
^\[main.assertion.6\] .* NotForall-NotForall: successful: SUCCESS$
11-
^\*\* 2 of 6 failed
11+
^\*\* 3 of 6 failed
1212
^VERIFICATION FAILED$
1313
^EXIT=10$
1414
^SIGNAL=0$
15+
--
16+
^warning: ignoring

‎regression/cbmc/Quantifiers-assignment/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,13 @@ int main()
44
a[0]=1;
55
a[1]=2;
66

7+
// clang-format off
8+
// clang-format would rewrite the "==>" as "== >"
79
int x=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 };
810
int y=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2 };
911
int z1=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<1.5 };
1012
int z2=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2*10 };
13+
// clang-format on
1114

1215
assert(x);
1316
assert(y);

‎regression/cbmc/Quantifiers-assignment/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,5 @@ main.c
1010
^VERIFICATION FAILED$
1111
^EXIT=10$
1212
^SIGNAL=0$
13+
--
14+
^warning: ignoring

‎regression/cbmc/Quantifiers-copy/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,10 @@ int main()
99
a[3]=3;
1010
a[4]=4;
1111

12+
// clang-format off
13+
// clang-format would rewrite the "==>" as "== >"
1214
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> b[i]==a[i]});
15+
// clang-format on
1316

1417
assert(b[0]==0);
1518
assert(b[1]==1);

‎regression/cbmc/Quantifiers-copy/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ main.c
1111
^VERIFICATION SUCCESSFUL$
1212
^EXIT=0$
1313
^SIGNAL=0$
14+
--
15+
^warning: ignoring

‎regression/cbmc/Quantifiers-if/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ int main()
44
a[0]=1;
55
a[1]=2;
66

7+
// clang-format off
8+
// clang-format would rewrite the "==>" as "== >"
79
if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
810
__CPROVER_assert(0, "failure 1");
911

@@ -18,6 +20,7 @@ int main()
1820

1921
if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
2022
__CPROVER_assert(0, "success 2");
23+
// clang-format on
2124

2225
return 0;
2326
}

‎regression/cbmc/Quantifiers-if/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ main.c
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$
14+
--
15+
^warning: ignoring

‎regression/cbmc/Quantifiers-initialisation/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,10 @@ int main()
22
{
33
int a[5];
44

5+
// clang-format off
6+
// clang-format would rewrite the "==>" as "== >"
57
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> a[i]==i+1});
8+
// clang-format on
69

710
assert(a[0]==1);
811
assert(a[1]==2);

‎regression/cbmc/Quantifiers-initialisation/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ main.c
1111
^VERIFICATION SUCCESSFUL$
1212
^EXIT=0$
1313
^SIGNAL=0$
14+
--
15+
^warning: ignoring

‎regression/cbmc/Quantifiers-initialisation2/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ int main()
33
int a[10];
44
int c[10];
55

6+
// clang-format off
7+
// clang-format would rewrite the "==>" as "== >"
68
// C# style
79
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<9+1) ==> a[i]>=1 && a[i]<=10 });
810
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<10) ==> __CPROVER_forall{int j; (j>i && j<10) ==> a[j]>a[i]} });
@@ -14,5 +16,6 @@ int main()
1416
assert(a[2]>a[3]);
1517
__CPROVER_assert(__CPROVER_forall {unsigned i; (i>=1 && i<10) ==> c[i-1]<=c[i]}, "forall c[]");
1618
assert(c[3]>=c[1]);
19+
// clang-format on
1720
return 0;
1821
}

‎regression/cbmc/Quantifiers-initialisation2/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ main.c
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$
14+
--
15+
^warning: ignoring

‎regression/cbmc/Quantifiers-invalid-var-range/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,10 @@ int main()
22
{
33

44
int a[3][3];
5+
// clang-format off
6+
// clang-format would rewrite the "==>" as "== >"
57
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> __CPROVER_exists{int j; (j>=i && j<3) ==> a[i][j]==10} });
8+
// clang-format on
69

710
assert(a[0][0]==10||a[0][1]==10||a[0][2]==10);
811

‎regression/cbmc/Quantifiers-invalid-var-range/test.desc

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^\*\* Results:$
55
^\*\* 0 of 1 failed
66
^VERIFICATION SUCCESSFUL$
77
^EXIT=0$
88
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--
12+
This produces the expected verification result, but actually ignores some
13+
quantifiers.

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

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
int main()
2+
{
3+
int a[2][2];
4+
int b[2][2];
5+
int c[2][2];
6+
int d[2][2];
7+
8+
// clang-format off
9+
// clang-format would rewrite the "==>" as "== >"
10+
// NOLINTNEXTLINE(whitespace/line_length)
11+
__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && a[i][j]<=10}) });
12+
13+
assert(0);
14+
15+
// NOLINTNEXTLINE(whitespace/line_length)
16+
__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}) });
17+
18+
assert(0);
19+
20+
// NOLINTNEXTLINE(whitespace/line_length)
21+
__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)}) });
22+
23+
assert(0);
24+
25+
// NOLINTNEXTLINE(whitespace/line_length)
26+
__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}) });
27+
// clang-format on
28+
29+
assert(0);
30+
31+
assert(a[0][0] > 10);
32+
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));
35+
36+
assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10);
37+
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)));
40+
41+
return 0;
42+
}

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
fixed.c
3+
4+
^\*\* 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$
11+
^\*\* 4 of 10 failed
12+
^VERIFICATION FAILED$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
--
16+
^warning: ignoring

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,24 @@ int main()
66
int c[2][2];
77
int d[2][2];
88

9+
// clang-format off
10+
// clang-format would rewrite the "==>" as "== >"
911
__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> a[i][j]<=10}) });
1012

13+
assert(0);
14+
1115
__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}) });
1216

17+
assert(0);
18+
1319
__CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });
1420

21+
assert(0);
22+
1523
__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}) });
24+
// clang-format on
1625

26+
assert(0);
1727

1828
assert(a[0][0]>10);
1929

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

Lines changed: 14 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,20 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^\*\* Results:$
5-
^\[main.assertion.1\] line 18 assertion a\[.*\]\[.*\] > 10: SUCCESS$
6-
^\[main.assertion.2\] line 20 assertion tmp_if_expr\$\d+: SUCCESS$
7-
^\[main.assertion.3\] line 21 assertion tmp_if_expr\$\d+: SUCCESS$
8-
^\[main.assertion.4\] line 23 assertion tmp_if_expr\$\d+: SUCCESS$
9-
^\[main.assertion.5\] line 25 assertion tmp_if_expr\$\d+: SUCCESS$
10-
^\[main.assertion.6\] line 26 assertion tmp_if_expr\$\d+: SUCCESS$
11-
^\*\* 0 of 6 failed
5+
^\[main.assertion.5\] line 28 assertion a\[.*\]\[.*\] > 10: SUCCESS$
6+
^\[main.assertion.6\] line 30 assertion tmp_if_expr\$\d+: SUCCESS$
7+
^\[main.assertion.7\] line 31 assertion tmp_if_expr\$\d+: SUCCESS$
8+
^\[main.assertion.8\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
9+
^\[main.assertion.9\] line 35 assertion tmp_if_expr\$\d+: SUCCESS$
10+
^\[main.assertion.10\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
11+
^\*\* 0 of 10 failed
1212
^VERIFICATION SUCCESSFUL$
1313
^EXIT=0$
1414
^SIGNAL=0$
15+
--
16+
^warning: ignoring
17+
--
18+
All assertions are unreachable as each of the __CPROVER_assume evaluate to false
19+
(!exists i. i>=0 && i<2 ==> ... is equivalent to forall i. i>=0 && i<2 && ...,
20+
where neither i>=0 nor i<2 is actually true for all values of i).

‎regression/cbmc/Quantifiers-not/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ int main()
44
a[0]=1;
55
a[1]=2;
66

7+
// clang-format off
8+
// clang-format would rewrite the "==>" as "== >"
79
if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
810
__CPROVER_assert(0, "success 1");
911

@@ -18,6 +20,7 @@ int main()
1820

1921
if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
2022
__CPROVER_assert(0, "failure 2");
23+
// clang-format on
2124

2225
return 0;
2326
}

‎regression/cbmc/Quantifiers-not/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ main.c
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$
14+
--
15+
^warning: ignoring

‎regression/cbmc/Quantifiers-two-dimension-array/fixed.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
int main()
2+
{
3+
int a[2][2];
4+
int b[2][2];
5+
6+
// clang-format off
7+
// clang-format would rewrite the "==>" as "== >"
8+
// NOLINTNEXTLINE(whitespace/line_length)
9+
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> a[i][j]==i+j}) });
10+
// NOLINTNEXTLINE(whitespace/line_length)
11+
__CPROVER_assume(__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && b[i][j]==i+j+1}) });
12+
// clang-format on
13+
14+
assert(a[0][0] == 0);
15+
assert(a[0][1] == 1);
16+
assert(a[1][0] == 1);
17+
assert(a[1][1] == 2);
18+
assert(b[0][0] == 1 || b[0][1] == 2 || b[1][0] == 2 || b[1][1] == 3);
19+
return 0;
20+
}

‎regression/cbmc/Quantifiers-two-dimension-array/fixed.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
fixed.c
3+
4+
^\*\* Results:$
5+
^\[main.assertion.1\] line 14 assertion a\[.*\]\[.*\] == 0: SUCCESS$
6+
^\[main.assertion.2\] line 15 assertion a\[.*\]\[.*\] == 1: SUCCESS$
7+
^\[main.assertion.3\] line 16 assertion a\[.*\]\[.*\] == 1: SUCCESS$
8+
^\[main.assertion.4\] line 17 assertion a\[.*\]\[.*\] == 2: SUCCESS$
9+
^\[main.assertion.5\] line 18 assertion tmp_if_expr\$\d+: SUCCESS$
10+
^\*\* 0 of 5 failed
11+
^VERIFICATION SUCCESSFUL$
12+
^EXIT=0$
13+
^SIGNAL=0$
14+
--
15+
^warning: ignoring

‎regression/cbmc/Quantifiers-two-dimension-array/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,11 @@ int main()
33
int a[2][2];
44
int b[2][2];
55

6+
// clang-format off
7+
// clang-format would rewrite the "==>" as "== >"
68
__CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> a[i][j]==i+j}) });
79
__CPROVER_assume(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]==i+j+1}) });
10+
// clang-format on
811

912
assert(a[0][0]==0);
1013
assert(a[0][1]==1);

‎regression/cbmc/Quantifiers-two-dimension-array/test.desc

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,18 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^\*\* Results:$
5-
^\[main.assertion.1\] line 9 assertion a\[.*\]\[.*\] == 0: SUCCESS$
6-
^\[main.assertion.2\] line 10 assertion a\[.*\]\[.*\] == 1: SUCCESS$
7-
^\[main.assertion.3\] line 11 assertion a\[.*\]\[.*\] == 1: SUCCESS$
8-
^\[main.assertion.4\] line 12 assertion a\[.*\]\[.*\] == 2: SUCCESS$
9-
^\[main.assertion.5\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
10-
^\*\* 0 of 5 failed
11-
^VERIFICATION SUCCESSFUL$
12-
^EXIT=0$
5+
^\[main.assertion.1\] line 12 assertion a\[.*\]\[.*\] == 0: SUCCESS$
6+
^\[main.assertion.2\] line 13 assertion a\[.*\]\[.*\] == 1: SUCCESS$
7+
^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$
8+
^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$
9+
^\[main.assertion.5\] line 16 assertion tmp_if_expr\$\d+: FAILURE$
10+
^\*\* 1 of 5 failed
11+
^VERIFICATION FAILED$
12+
^EXIT=10$
1313
^SIGNAL=0$
14+
--
15+
^warning: ignoring
16+
--
17+
The assertion on line 13 need not hold as the assume can be satisfied by picking
18+
a value for i that does not fulfil the left-hand side of the implication.

‎regression/cbmc/Quantifiers-type/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,11 @@ int main()
33
int a[2];
44
int b[2];
55

6+
// clang-format off
7+
// clang-format would rewrite the "==>" as "== >"
68
__CPROVER_assume( __CPROVER_forall { float i; (i>=0 && i<2) ==> a[i]>=10 && a[i]<=10 } );
79
__CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
10+
// clang-format on
811

912
assert(a[0]==10 && a[1]==10);
1013
assert(b[0]==10 && b[1]==10);

0 commit comments

Comments
 (0)