Skip to content

Commit 052c149

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #1255 from peterschrammel/bugfix/java-unambiguous-basic-blocks
Improve bytecode-instrumentability of basic blocks
2 parents f39e5ab + b6ef688 commit 052c149

File tree

37 files changed

+468
-222
lines changed

37 files changed

+468
-222
lines changed

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ DIRS = ansi-c \
33
cpp \
44
cbmc-java \
55
cbmc-java-inheritance \
6+
cbmc-cover \
67
goto-analyzer \
78
goto-diff \
89
goto-instrument \

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ int main()
55
__CPROVER_input("input1", input1);
66
__CPROVER_input("input2", input2);
77

8+
// assert() is platform-dependent and changes set of coverage goals
89
__CPROVER_assert(!input1, "");
910

1011
if(input1)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover assertion
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 8 function main: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 12 function main: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 9 function main: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 13 function main: SATISFIED$
88
--
99
^warning: ignoring

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ main.c
33
--cover branch
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 3 function main function main entry point: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 8 function main function main block 1 branch false: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 8 function main function main block 1 branch true: SATISFIED$
9-
^\[main.coverage.4\] file main.c line 10 function main function main block 2 branch false: FAILED$
10-
^\[main.coverage.5\] file main.c line 10 function main function main block 2 branch true: SATISFIED$
11-
^\[main.coverage.6\] file main.c line 16 function main function main block 4 branch false: SATISFIED$
12-
^\[main.coverage.7\] file main.c line 16 function main function main block 4 branch true: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 3 function main entry point: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 8 function main block 1 branch false: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 8 function main block 1 branch true: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 10 function main block 2 branch false: FAILED$
10+
^\[main.coverage.5\] file main.c line 10 function main block 2 branch true: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 16 function main block 4 branch false: SATISFIED$
12+
^\[main.coverage.7\] file main.c line 16 function main block 4 branch true: SATISFIED$
1313
--
1414
^warning: ignoring

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--cover branch --unwind 2
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 5 function main function main entry point: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 6 function main function main block .* branch false: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 6 function main function main block .* branch true: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 5 function main entry point: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 6 function main block .* branch false: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 6 function main block .* branch true: SATISFIED$
99
--
1010
^warning: ignoring

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21
#include <stdio.h>
32

43
int main()

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33
--cover branch --unwind 6
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 23 of 23 covered \(100.0%\)$
6+
^\*\* .* of .* covered \(100.0%\)$
77
--
88
^warning: ignoring

‎regression/cbmc-cover/built-ins2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover location --unwind 10
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 4 of 4 covered
6+
^\*\* .* of .* covered \(100.0%\)
77
--
88
^warning: ignoring
99
^\[.*<builtin-library-

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,5 +14,6 @@ int main()
1414
}
1515

1616
// should not produce a goal
17+
// assert() is platform-dependent and changes set of coverage goals
1718
__CPROVER_assert(input1, "");
1819
}

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--cover branch
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[my_func.coverage.1\] file main.c line 3 function my_func function my_func block 1 branch false: SATISFIED$
7-
^\[my_func.coverage.2\] file main.c line 3 function my_func function my_func block 1 branch true: FAILED$
8-
^\[my_func.coverage.3\] file main.c line 3 function my_func function my_func block 2 branch false: FAILED$
9-
^\[my_func.coverage.4\] file main.c line 3 function my_func function my_func block 2 branch true: SATISFIED$
6+
^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
7+
^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
8+
^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
9+
^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
1010
--
1111
^warning: ignoring

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int myfunc(int x, int y)
42
{
53
int z = x + y;

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

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,15 @@ main.c
33
--cover location
44
^EXIT=0$
55
^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 4: SATISFIED$
10-
^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
11-
^\[main.coverage.6\] file main.c line 18 function main block 6: SATISFIED$
12-
^\[main.coverage.7\] file main.c line 20 function main block 7: FAILED$
13-
^\[main.coverage.8\] file main.c line 22 function main block 8: SATISFIED$
14-
^\[main.coverage.9\] file main.c line 23 function main block 9: 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%\)
6+
^\[main.coverage.1\] file main.c line 9 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main block 2: FAILED$
8+
^\[main.coverage.3\] file main.c line 11 function main block 3: FAILED$
9+
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 15 function main block 5: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 16 function main block 6: SATISFIED$
12+
^\[main.coverage.7\] file main.c line 18 function main block 7: FAILED$
13+
^\[main.coverage.8\] file main.c line 20 function main block 8: SATISFIED$
14+
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1: FAILED$
15+
^\*\* 5 of 9 covered \(55.6%\)
1816
--
1917
^warning: ignoring

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int foo (int iX, int iY)
42
{
53
return iX + iY;

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

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

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int myfunc(int a, int b)
42
{
53
return a+b;

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

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

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int foo (int iX, int iY)
42
{
53
return iX + iY;
@@ -9,5 +7,7 @@ int main(void)
97
{
108
int iN = 2 + 1;
119
if (iN == 4)
12-
assert(foo(5,3)==8);
10+
11+
// assert() is platform-dependent and changes set of coverage goals
12+
__CPROVER_assert(foo(5,3)==8, "");
1313
}

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

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

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21
#include <math.h>
32

43
int foo (int iX, int iY)

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

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,13 @@
1-
KNOWNBUG
1+
THOROUGH
22
main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
77
^\[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%\)
8+
^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
9+
^\[main.coverage.4\] file main.c line 16 function main block 4: SATISFIED$
10+
^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
11+
^\*\* 3 of 5 covered \(60.0%\)
1612
--
1713
^warning: ignoring

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int func(int a)
42
{
53
int b = a*2;
@@ -10,7 +8,8 @@ int func(int a)
108
b += 10;
119
}
1210

13-
assert(0);
11+
// assert() is platform-dependent and changes set of coverage goals
12+
__CPROVER_assert(0, "");
1413

1514
return b;
1615
}

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

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,13 @@ main.c
33
--cover location
44
^EXIT=0$
55
^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%\)
6+
^\[main.coverage.1\] file main.c line 19 function main block 1: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 20 function main block 2: SATISFIED$
8+
^\[func.coverage.1\] file main.c line 3 function func block 1: SATISFIED$
9+
^\[func.coverage.2\] file main.c line 6 function func block 2: FAILED$
10+
^\[func.coverage.3\] file main.c line 8 function func block 3: FAILED$
11+
^\[func.coverage.4\] file main.c line 12 function func block 4: FAILED$
12+
^\[func.coverage.5\] file main.c line 15 function func block 5: SATISFIED$
13+
^\*\* 4 of 7 covered \(57.1%\)
1614
--
1715
^warning: ignoring

‎regression/cbmc-cover/unique-bytecode1/Test.class

301 Bytes
Binary file not shown.

‎regression/cbmc-cover/unique-bytecode1/Test.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
class Test {
2+
public static void main(String[] args) {
3+
for (int i=0; i<3; i++) {
4+
}
5+
}
6+
}

‎regression/cbmc-cover/unique-bytecode1/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
Test.class
3+
--cover location --show-properties --verbosity 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^Ignoring block .* java::Test\.main

‎regression/cbmc-cover/unique-bytecode2/Test.class

262 Bytes
Binary file not shown.

‎regression/cbmc-cover/unique-bytecode2/Test.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
class Test {
2+
static int s=5;
3+
}

‎regression/cbmc-cover/unique-bytecode2/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Test.class
3+
--cover location --show-properties --verbosity 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^java::Test\.<clinit>:\(\)V block 2, location 4: bytecode-index 1 already instrumented
7+
^Ignoring block 2 location .* file Test\.java line 2 function java::Test\.<clinit>:\(\)V bytecode-index .* \(bytecode-index already instrumented\)
8+
--

‎regression/cbmc-cover/unique-bytecode3/Test.class

292 Bytes
Binary file not shown.

‎regression/cbmc-cover/unique-bytecode3/Test.java

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
class Test {
2+
static int x = 0;
3+
static int y = 1;
4+
}

‎regression/cbmc-cover/unique-bytecode3/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--cover location --show-properties --verbosity 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^java::Test\.<clinit>:\(\)V block 2, location 4: bytecode-index 1 already instrumented
7+
^java::Test\.<clinit>:\(\)V block 2: location 5, bytecode-index 3 selected for instrumentation
8+
--
9+
^Ignoring block 2 location .* file Test\.java line 3 function java::Test\.<clinit>:\(\)V bytecode-index .* \(bytecode-index already instrumented\)

‎src/cbmc/bmc_cover.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,8 @@ void bmc_covert::satisfying_assignment()
161161

162162
if(solver.l_get(cond).is_true())
163163
{
164-
status() << "Covered " << g.description << messaget::eom;
164+
status() << "Covered function " << g.source_location.get_function()
165+
<< " " << g.description << messaget::eom;
165166
g.satisfied=true;
166167
test.covered_goals.push_back(goal_pair.first);
167168
break;

0 commit comments

Comments
 (0)