Skip to content

Commit d9d04bf

Browse files
author
Daniel Kroening
authored
Merge pull request #290 from lucasccordeiro/siemens_fix255_squashed
add test cases to check the behaviour of --cover in the presence of u…
2 parents f3c02c4 + 7cc49cf commit d9d04bf

File tree

12 files changed

+203
-0
lines changed

12 files changed

+203
-0
lines changed

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <assert.h>
2+
3+
int myfunc(int x, int y)
4+
{
5+
int z = x + y;
6+
return z;
7+
}
8+
9+
int main(void)
10+
{
11+
_Bool x=0, y;
12+
if (x)
13+
assert(myfunc(2,3)==5);
14+
else
15+
y=1;
16+
17+
if (y)
18+
y=0;
19+
else
20+
__CPROVER_assume(0);
21+
22+
assert(y==1);
23+
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE
2+
main.c
3+
--cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 13 function main block 2: FAILED$
8+
^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
9+
^\[main.coverage.4\] file main.c line 15 function main block 5: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 17 function main block 6: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 18 function main block 7: SATISFIED$
12+
^\[main.coverage.7\] file main.c line 20 function main block 8: FAILED$
13+
^\[main.coverage.8\] file main.c line 22 function main block 9: SATISFIED$
14+
^\[main.coverage.9\] file main.c line 23 function main block 10: SATISFIED$
15+
^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
16+
^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
17+
^\*\* 6 of 11 covered (54.5%)
18+
--
19+
^warning: ignoring

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
3+
int foo (int iX, int iY)
4+
{
5+
return iX + iY;
6+
__CPROVER_assume(0);
7+
}
8+
9+
int main(void)
10+
{
11+
assert(foo(5,3)==8);
12+
}

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 12 function main block 3: SATISFIED$
9+
^\[foo.coverage.1\] file main.c line 5 function foo block 1: SATISFIED$
10+
^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
11+
^\[foo.coverage.3\] file main.c line 7 function foo block 3: FAILED$
12+
^\[foo.coverage.4\] file main.c line 7 function foo block 4: SATISFIED$
13+
^\*\* 5 of 7 covered (71.4%)
14+
--
15+
^warning: ignoring

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
3+
int myfunc(int a, int b)
4+
{
5+
return a+b;
6+
}
7+
8+
int foo (int iX, int iY)
9+
{
10+
return iX + iY;
11+
assert(myfunc(iX,iY)==8);
12+
}
13+
14+
int main(void)
15+
{
16+
assert(foo(5,3)==8);
17+
}

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 16 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 16 function main block 2: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 17 function main block 3: SATISFIED$
9+
^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
10+
^\[myfunc.coverage.2\] file main.c line 6 function myfunc block 2: FAILED$
11+
^\[foo.coverage.1\] file main.c line 10 function foo block 1: SATISFIED$
12+
^\[foo.coverage.2\] file main.c line 11 function foo block 2: FAILED$
13+
^\[foo.coverage.3\] file main.c line 11 function foo block 3: FAILED$
14+
^\[foo.coverage.4\] file main.c line 12 function foo block 4: FAILED$
15+
^\[foo.coverage.5\] file main.c line 12 function foo block 5: SATISFIED$
16+
^\*\* 5 of 10 covered (50.0%)
17+
--
18+
^warning: ignoring

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int foo (int iX, int iY)
4+
{
5+
return iX + iY;
6+
}
7+
8+
int main(void)
9+
{
10+
int iN = 2 + 1;
11+
if (iN == 4)
12+
assert(foo(5,3)==8);
13+
}

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 12 function main block 2: FAILED$
8+
^\[main.coverage.3\] file main.c line 12 function main block 3: FAILED$
9+
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
10+
^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
11+
^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
12+
^\*\* 2 of 6 covered (33.3%)
13+
--
14+
^warning: ignoring

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
#include <math.h>
3+
4+
int foo (int iX, int iY)
5+
{
6+
return iX + iY;
7+
}
8+
9+
int main(void)
10+
{
11+
double dX = sqrt(2);
12+
if (dX > 5)
13+
{
14+
__CPROVER_assume(0);
15+
assert(foo(5,3)==1);
16+
}
17+
}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 14 function main block 3: FAILED$
9+
^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
10+
^\[main.coverage.5\] file main.c line 15 function main block 5: FAILED$
11+
^\[main.coverage.6\] file main.c line 16 function main block 6: FAILED$
12+
^\[main.coverage.7\] file main.c line 17 function main block 7: SATISFIED$
13+
^\[foo.coverage.1\] file main.c line 6 function foo block 1: FAILED$
14+
^\[foo.coverage.2\] file main.c line 7 function foo block 2: FAILED$
15+
^\*\* 3 of 9 covered (33.3%)
16+
--
17+
^warning: ignoring

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
#include <assert.h>
2+
3+
int func(int a)
4+
{
5+
int b = a*2;
6+
return b;
7+
8+
if (b < 10)
9+
{
10+
b += 10;
11+
}
12+
13+
assert(0);
14+
15+
return b;
16+
}
17+
18+
int main(void)
19+
{
20+
func(2);
21+
}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 20 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 21 function main block 2: SATISFIED$
8+
^\[func.coverage.1\] file main.c line 5 function func block 1: SATISFIED$
9+
^\[func.coverage.2\] file main.c line 8 function func block 2: FAILED$
10+
^\[func.coverage.3\] file main.c line 10 function func block 3: FAILED$
11+
^\[func.coverage.4\] file main.c line 13 function func block 4: FAILED$
12+
^\[func.coverage.5\] file main.c line 13 function func block 5: FAILED$
13+
^\[func.coverage.6\] file main.c line 15 function func block 6: FAILED$
14+
^\[func.coverage.7\] file main.c line 16 function func block 7: SATISFIED$
15+
^\*\* 4 of 9 covered (44.4%)
16+
--
17+
^warning: ignoring

0 commit comments

Comments
 (0)