Skip to content

Commit ee35009

Browse files
Tuttletautschnig
Tuttle
authored and
tautschnig
committed
Added basic block source lines to source_locationt
Block coverage obtained with "cbmc --cover locations" now reports the file name and line number of every line of source code contributing to a basic block in the "description" field of the xml output. (The lines contributing to a block can come from multiple files via function inlining and definitions in include files, so reporting line numbers alone is not sufficient.)
1 parent 7f2ff2c commit ee35009

File tree

27 files changed

+280
-47
lines changed

27 files changed

+280
-47
lines changed

‎jbmc/regression/jdiff/java-properties/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location
55
activate-multi-line-match
66
EXIT=0
77
SIGNAL=0
8-
"deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.<init>:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.<clinit>:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.<clinit>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n
8+
"deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1 \(lines \)",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.<init>:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2 \(lines \)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3 \(lines \)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4 \(lines \)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5 \(lines \)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6 \(lines \)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.<clinit>:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1 \(lines \)",\n "expression": "false",\n "name": "java::Test.<clinit>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1 \(lines \)",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n
99
--
1010
^warning: ignoring

‎regression/cbmc-cover/block-coverage-report1/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int main()
2+
{
3+
int x;
4+
5+
if(x < 0)
6+
return 0;
7+
else
8+
return 1;
9+
}

‎regression/cbmc-cover/block-coverage-report1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--cover location
4+
block 1 \(lines main.c:main:3,5\): SATISFIED
5+
block 2 \(lines main.c:main:6\): SATISFIED
6+
block 3 \(lines main.c:main:6,9\): FAILED
7+
block 4 \(lines main.c:main:8\): SATISFIED
8+
block 5 \(lines main.c:main:9\): SATISFIED
9+
--

‎regression/cbmc-cover/block-coverage-report2/main.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// This is supposed to be testing basic blocks with inlining,
2+
// but cbmc has now turned off inlining by default.
3+
4+
inline int foo(int x)
5+
{
6+
int y;
7+
y = x + 1;
8+
return y;
9+
}
10+
11+
main()
12+
{
13+
int x;
14+
x = 10;
15+
while(x)
16+
{
17+
int y;
18+
y = foo(x);
19+
if(y < 5)
20+
break;
21+
x--;
22+
}
23+
24+
return;
25+
}

‎regression/cbmc-cover/block-coverage-report2/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--cover location
4+
block 1 \(lines main.c:main:13,14\): SATISFIED
5+
block 2 \(lines main.c:main:15\): SATISFIED
6+
block 3 \(lines main.c:main:17,18\): SATISFIED
7+
block 4 \(lines main.c:main:18,19\): SATISFIED
8+
block 5 \(lines main.c:main:20\): SATISFIED
9+
block 6 \(lines main.c:main:15,21,22\): SATISFIED
10+
block 7 \(lines main.c:main:24,25\): SATISFIED
11+
block 1 \(lines main.c:foo:6,7,8,9\): SATISFIED
12+
--

‎regression/cbmc-cover/block-coverage-report3/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
void main()
2+
{
3+
int x = 0;
4+
while(x < 3)
5+
{
6+
x++;
7+
}
8+
}

‎regression/cbmc-cover/block-coverage-report3/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--cover location --unwind 1
4+
block 1 \(lines main.c:main:3\): SATISFIED
5+
block 2 \(lines main.c:main:4\): SATISFIED
6+
block 3 \(lines main.c:main:4,6\): SATISFIED
7+
block 4 \(lines main.c:main:8\): FAILED
8+
--

‎regression/cbmc-cover/block-coverage-report4/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
void main()
2+
{
3+
int x = 0;
4+
while(x < 3)
5+
{
6+
x++;
7+
}
8+
}

‎regression/cbmc-cover/block-coverage-report4/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--cover location --unwind 4
4+
block 1 \(lines main.c:main:3\): SATISFIED
5+
block 2 \(lines main.c:main:4\): SATISFIED
6+
block 3 \(lines main.c:main:4,6\): SATISFIED
7+
block 4 \(lines main.c:main:8\): SATISFIED
8+
--

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

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

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
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$
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$
1515
^\*\* 5 of 9 covered \(55.6%\)
1616
--
1717
^warning: ignoring

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
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$
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$
1111
^\*\* 4 of 5 covered \(80.0%\)
1212
--
1313
^warning: ignoring

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

Lines changed: 7 additions & 7 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 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$
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$
1313
^\*\* 4 of 7 covered \(57.1%\)
1414
--
1515
^warning: ignoring

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 8 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 3 function foo block 1: FAILED$
6+
^\[main.coverage.1\] file main.c line 8 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 3 function foo block 1.*: FAILED$
1111
^\*\* 2 of 5 covered \(40.0%\)
1212
--
1313
^warning: ignoring

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +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$
7-
^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
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$
6+
^\[main.coverage.1\] file main.c line 10 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 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$
1111
^\*\* 3 of 5 covered \(60.0%\)
1212
--
1313
^warning: ignoring

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

Lines changed: 7 additions & 7 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 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$
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$
1313
^\*\* 4 of 7 covered \(57.1%\)
1414
--
1515
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.coverage\.1\] .* function main block 1: SATISFIED$
6+
^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$
77
(1 of 1|3 of 3) covered \(100\.0%\)$
88
--
99
^warning: ignoring
1010
^CONVERSION ERROR$
11-
^\[main\.coverage\..\] .* function main block .: FAILED$
11+
^\[main\.coverage\..\] .* function main block .*: FAILED$
1212
--
1313
On Windows/Visual Studio, "assert" does not introduce any branching.

‎src/cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
2626
../pointer-analysis/add_failed_symbols$(OBJEXT) \
2727
../pointer-analysis/rewrite_index$(OBJEXT) \
2828
../pointer-analysis/goto_program_dereference$(OBJEXT) \
29+
../goto-instrument/source_lines$(OBJEXT) \
2930
../goto-instrument/cover$(OBJEXT) \
3031
../goto-instrument/cover_basic_blocks$(OBJEXT) \
3132
../goto-instrument/cover_filter$(OBJEXT) \

‎src/goto-diff/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1414
../goto-programs/goto-programs$(LIBEXT) \
1515
../assembler/assembler$(LIBEXT) \
1616
../pointer-analysis/pointer-analysis$(LIBEXT) \
17+
../goto-instrument/source_lines$(OBJEXT) \
1718
../goto-instrument/cover$(OBJEXT) \
1819
../goto-instrument/cover_basic_blocks$(OBJEXT) \
1920
../goto-instrument/cover_filter$(OBJEXT) \

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ SRC = accelerate/accelerate.cpp \
5757
rw_set.cpp \
5858
show_locations.cpp \
5959
skip_loops.cpp \
60+
source_lines.cpp \
6061
splice_call.cpp \
6162
stack_depth.cpp \
6263
thread_instrumentation.cpp \

0 commit comments

Comments
 (0)