replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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.)
This commit is contained in:
Tuttle 2018-02-23 17:24:30 -05:00 committed by Michael Tautschnig
parent 85a2a6a948
commit 01f4ee2672
31 changed files with 309 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
jbmc/regression/jdiff/java-properties/test.desc
View File

@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location
activate-multi-line-match
EXIT=0
SIGNAL=0
"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
"deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\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 Test.java:java::Test.<init>:\(\)V:6\)",\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 Test.java:java::Test.<init>:\(\)V:4\)",\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 Test.java:java::Test.<init>:\(\)V: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 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\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 Test.java:java::Test.<init>:\(\)V:7\)",\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 Test.java:java::Test.<clinit>:\(\)V:3\)",\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 Test.java:java::Test.newfun:\(\)V:18\)",\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
--
^warning: ignoring

1
jbmc/src/jbmc/Makefile
View File

@ -20,6 +20,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
../$(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/source_lines$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \

1
jbmc/src/jdiff/Makefile
View File

@ -14,6 +14,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
../$(CPROVER_DIR)/src/goto-diff/unified_diff$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-diff/change_impact$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-diff/goto_diff_base$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/source_lines$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \

1
jbmc/unit/Makefile
View File

@ -111,6 +111,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
$(CPROVER_DIR)/src/goto-instrument/source_lines$(OBJEXT) \
$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \

9
regression/cbmc-cover/block-coverage-report1/main.c Normal file
View File

@ -0,0 +1,9 @@
int main()
{
int x;
if(x < 0)
return 0;
else
return 1;
}

9
regression/cbmc-cover/block-coverage-report1/test.desc Normal file
View File

@ -0,0 +1,9 @@
CORE
main.c
--cover location
block 1 \(lines main.c:main:3,5\): SATISFIED
block 2 \(lines main.c:main:6\): SATISFIED
block 3 \(lines main.c:main:6,9\): FAILED
block 4 \(lines main.c:main:8\): SATISFIED
block 5 \(lines main.c:main:9\): SATISFIED
--

25
regression/cbmc-cover/block-coverage-report2/main.c Normal file
View File

@ -0,0 +1,25 @@
// This is supposed to be testing basic blocks with inlining,
// but cbmc has now turned off inlining by default.
inline int foo(int x)
{
int y;
y = x + 1;
return y;
}
main()
{
int x;
x = 10;
while(x)
{
int y;
y = foo(x);
if(y < 5)
break;
x--;
}
return;
}

12
regression/cbmc-cover/block-coverage-report2/test.desc Normal file
View File

@ -0,0 +1,12 @@
CORE
main.c
--cover location
block 1 \(lines main.c:main:13,14\): SATISFIED
block 2 \(lines main.c:main:15\): SATISFIED
block 3 \(lines main.c:main:17,18\): SATISFIED
block 4 \(lines main.c:main:18,19\): SATISFIED
block 5 \(lines main.c:main:20\): SATISFIED
block 6 \(lines main.c:main:15,21,22\): SATISFIED
block 7 \(lines main.c:main:24,25\): SATISFIED
block 1 \(lines main.c:foo:6-9\): SATISFIED
--

8
regression/cbmc-cover/block-coverage-report3/main.c Normal file
View File

@ -0,0 +1,8 @@
void main()
{
int x = 0;
while(x < 3)
{
x++;
}
}

8
regression/cbmc-cover/block-coverage-report3/test.desc Normal file
View File

@ -0,0 +1,8 @@
CORE
main.c
--cover location --unwind 1
block 1 \(lines main.c:main:3\): SATISFIED
block 2 \(lines main.c:main:4\): SATISFIED
block 3 \(lines main.c:main:4,6\): SATISFIED
block 4 \(lines main.c:main:8\): FAILED
--

8
regression/cbmc-cover/block-coverage-report4/main.c Normal file
View File

@ -0,0 +1,8 @@
void main()
{
int x = 0;
while(x < 3)
{
x++;
}
}

8
regression/cbmc-cover/block-coverage-report4/test.desc Normal file
View File

@ -0,0 +1,8 @@
CORE
main.c
--cover location --unwind 4
block 1 \(lines main.c:main:3\): SATISFIED
block 2 \(lines main.c:main:4\): SATISFIED
block 3 \(lines main.c:main:4,6\): SATISFIED
block 4 \(lines main.c:main:8\): SATISFIED
--

10
regression/cbmc-cover/location1/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 3 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main block 2: SATISFIED$
^\[main.coverage.3\] file main.c line 13 function main block 3: SATISFIED$
^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
^\[main.coverage.1\] file main.c line 3 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
^\[main.coverage.3\] file main.c line 13 function main block 3.*: SATISFIED$
^\[main.coverage.4\] file main.c line 15 function main block 4.*: FAILED$
^\[main.coverage.5\] file main.c line 17 function main block 5.*: SATISFIED$
^\*\* 4 of 5 covered \(80.0%\)
--
^warning: ignoring

18
regression/cbmc-cover/location11/test.desc
View File

@ -3,15 +3,15 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 9 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 11 function main block 2: FAILED$
^\[main.coverage.3\] file main.c line 11 function main block 3: FAILED$
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
^\[main.coverage.5\] file main.c line 15 function main block 5: SATISFIED$
^\[main.coverage.6\] file main.c line 16 function main block 6: SATISFIED$
^\[main.coverage.7\] file main.c line 18 function main block 7: FAILED$
^\[main.coverage.8\] file main.c line 20 function main block 8: SATISFIED$
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1: FAILED$
^\[main.coverage.1\] file main.c line 9 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 11 function main block 2.*: FAILED$
^\[main.coverage.3\] file main.c line 11 function main block 3.*: FAILED$
^\[main.coverage.4\] file main.c line 13 function main block 4.*: SATISFIED$
^\[main.coverage.5\] file main.c line 15 function main block 5.*: SATISFIED$
^\[main.coverage.6\] file main.c line 16 function main block 6.*: SATISFIED$
^\[main.coverage.7\] file main.c line 18 function main block 7.*: FAILED$
^\[main.coverage.8\] file main.c line 20 function main block 8.*: SATISFIED$
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1.*: FAILED$
^\*\* 5 of 9 covered \(55.6%\)
--
^warning: ignoring

10
regression/cbmc-cover/location12/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 9 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main block 2: SATISFIED$
^\[foo.coverage.1\] file main.c line 3 function foo block 1: SATISFIED$
^\[foo.coverage.2\] file main.c line 4 function foo block 2: FAILED$
^\[foo.coverage.3\] file main.c line 5 function foo block 3: SATISFIED$
^\[main.coverage.1\] file main.c line 9 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$
^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$
^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$
^\*\* 4 of 5 covered \(80.0%\)
--
^warning: ignoring

14
regression/cbmc-cover/location13/test.desc
View File

@ -3,13 +3,13 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 14 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 15 function main block 2: SATISFIED$
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1: FAILED$
^\[foo.coverage.1\] file main.c line 8 function foo block 1: SATISFIED$
^\[foo.coverage.2\] file main.c line 9 function foo block 2: FAILED$
^\[foo.coverage.3\] file main.c line 10 function foo block 3: FAILED$
^\[foo.coverage.4\] file main.c line 10 function foo block 4: SATISFIED$
^\[main.coverage.1\] file main.c line 14 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 15 function main block 2.*: SATISFIED$
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1.*: FAILED$
^\[foo.coverage.1\] file main.c line 8 function foo block 1.*: SATISFIED$
^\[foo.coverage.2\] file main.c line 9 function foo block 2.*: FAILED$
^\[foo.coverage.3\] file main.c line 10 function foo block 3.*: FAILED$
^\[foo.coverage.4\] file main.c line 10 function foo block 4.*: SATISFIED$
^\*\* 4 of 7 covered \(57.1%\)
--
^warning: ignoring

10
regression/cbmc-cover/location14/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 8 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 12 function main block 2: FAILED$
^\[main.coverage.3\] file main.c line 12 function main block 3: FAILED$
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
^\[foo.coverage.1\] file main.c line 3 function foo block 1: FAILED$
^\[main.coverage.1\] file main.c line 8 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 12 function main block 2.*: FAILED$
^\[main.coverage.3\] file main.c line 12 function main block 3.*: FAILED$
^\[main.coverage.4\] file main.c line 13 function main block 4.*: SATISFIED$
^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: FAILED$
^\*\* 2 of 5 covered \(40.0%\)
--
^warning: ignoring

10
regression/cbmc-cover/location15/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
^\[main.coverage.4\] file main.c line 16 function main block 4: SATISFIED$
^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 11 function main block 2.*: SATISFIED$
^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$
^\*\* 3 of 5 covered \(60.0%\)
--
^warning: ignoring

14
regression/cbmc-cover/location16/test.desc
View File

@ -3,13 +3,13 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 19 function main block 1: SATISFIED$
^\[main.coverage.2\] file main.c line 20 function main block 2: SATISFIED$
^\[func.coverage.1\] file main.c line 3 function func block 1: SATISFIED$
^\[func.coverage.2\] file main.c line 6 function func block 2: FAILED$
^\[func.coverage.3\] file main.c line 8 function func block 3: FAILED$
^\[func.coverage.4\] file main.c line 12 function func block 4: FAILED$
^\[func.coverage.5\] file main.c line 15 function func block 5: SATISFIED$
^\[main.coverage.1\] file main.c line 19 function main block 1.*: SATISFIED$
^\[main.coverage.2\] file main.c line 20 function main block 2.*: SATISFIED$
^\[func.coverage.1\] file main.c line 3 function func block 1.*: SATISFIED$
^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$
^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$
^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$
^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$
^\*\* 4 of 7 covered \(57.1%\)
--
^warning: ignoring

4
regression/cbmc-cover/simple_assert/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main\.coverage\.1\] .* function main block 1: SATISFIED$
^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$
(1 of 1|3 of 3) covered \(100\.0%\)$
--
^warning: ignoring
^CONVERSION ERROR$
^\[main\.coverage\..\] .* function main block .: FAILED$
^\[main\.coverage\..\] .* function main block .*: FAILED$
--
On Windows/Visual Studio, "assert" does not introduce any branching.

1
src/cbmc/Makefile
View File

@ -26,6 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../pointer-analysis/add_failed_symbols$(OBJEXT) \
../pointer-analysis/rewrite_index$(OBJEXT) \
../pointer-analysis/goto_program_dereference$(OBJEXT) \
../goto-instrument/source_lines$(OBJEXT) \
../goto-instrument/cover$(OBJEXT) \
../goto-instrument/cover_basic_blocks$(OBJEXT) \
../goto-instrument/cover_filter$(OBJEXT) \

1
src/goto-diff/Makefile
View File

@ -14,6 +14,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../goto-programs/goto-programs$(LIBEXT) \
../assembler/assembler$(LIBEXT) \
../pointer-analysis/pointer-analysis$(LIBEXT) \
../goto-instrument/source_lines$(OBJEXT) \
../goto-instrument/cover$(OBJEXT) \
../goto-instrument/cover_basic_blocks$(OBJEXT) \
../goto-instrument/cover_filter$(OBJEXT) \

1
src/goto-instrument/Makefile
View File

@ -57,6 +57,7 @@ SRC = accelerate/accelerate.cpp \
rw_set.cpp \
show_locations.cpp \
skip_loops.cpp \
source_lines.cpp \
splice_call.cpp \
stack_depth.cpp \
thread_instrumentation.cpp \

35
src/goto-instrument/cover_basic_blocks.cpp
View File

@ -61,7 +61,10 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
// update lines belonging to block
const irep_idt &line = it->source_location.get_line();
if(!line.empty())
{
block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
block_info.source_lines.insert(it->source_location);
}
// set representative program location to instrument
if(
@ -84,7 +87,10 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
}
for(auto &block_info : block_infos)
{
update_covered_lines(block_info);
update_source_lines(block_info);
}
}
std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const
@ -162,19 +168,46 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
block_info.source_location.set_basic_block_covered_lines(covered_lines);
}
void cover_basic_blockst::update_source_lines(block_infot &block_info)
{
if(block_info.source_location.is_nil())
return;
const auto &source_lines = block_info.source_lines;
std::string str = source_lines.to_string();
INVARIANT(!str.empty(), "source lines set must not be empty");
block_info.source_location.set_basic_block_source_lines(str);
}
cover_basic_blocks_javat::cover_basic_blocks_javat(
const goto_programt &_goto_program)
{
std::set<std::size_t> source_lines_requiring_update;
forall_goto_program_instructions(it, _goto_program)
{
const auto &location = it->source_location;
const auto &bytecode_index = location.get_java_bytecode_index();
if(index_to_block.emplace(bytecode_index, block_infos.size()).second)
auto entry = index_to_block.emplace(bytecode_index, block_infos.size());
if(entry.second)
{
block_infos.push_back(it);
block_locations.push_back(location);
block_locations.back().set_basic_block_covered_lines(location.get_line());
block_source_lines.emplace_back(location);
source_lines_requiring_update.insert(entry.first->second);
}
else
{
block_source_lines[entry.first->second].insert(location);
source_lines_requiring_update.insert(entry.first->second);
}
}
for(std::size_t i : source_lines_requiring_update)
{
block_locations.at(i).set_basic_block_source_lines(
block_source_lines.at(i).to_string());
}
}

11
src/goto-instrument/cover_basic_blocks.h
View File

@ -18,6 +18,8 @@ Author: Daniel Kroening
#include <goto-programs/goto_model.h>
#include "source_lines.h"
class cover_blocks_baset
{
public:
@ -107,6 +109,9 @@ private:
/// the set of lines belonging to this block
std::unordered_set<std::size_t> lines;
/// the set of source code lines belonging to this block
source_linest source_lines;
};
/// map program locations to block numbers
@ -118,6 +123,10 @@ private:
/// location of basic block, compress to ranges if applicable
static void update_covered_lines(block_infot &block_info);
/// create a string representing source lines and set as a property of source
/// location of basic block
static void update_source_lines(block_infot &block_info);
/// If this block is a continuation of a previous block through unconditional
/// forward gotos, return this blocks number.
static optionalt<std::size_t> continuation_of_block(
@ -134,6 +143,8 @@ private:
std::vector<source_locationt> block_locations;
// map java indexes to block indexes
std::unordered_map<irep_idt, std::size_t> index_to_block;
// map block number to its source lines
std::vector<source_linest> block_source_lines;
public:
explicit cover_basic_blocks_javat(const goto_programt &_goto_program);

5
src/goto-instrument/cover_instrument_location.cpp
View File

@ -35,7 +35,10 @@ void cover_location_instrumentert::instrument(
// filter goals
if(goal_filters(source_location))
{
const std::string comment = "block " + b;
const std::string source_lines =
id2string(source_location.get_basic_block_source_lines());
const std::string comment =
"block " + b + " (lines " + source_lines + ")";
goto_program.insert_before_swap(i_it);
i_it->make_assertion(false_exprt());
i_it->source_location = source_location;

49
src/goto-instrument/source_lines.cpp Normal file
View File

@ -0,0 +1,49 @@
/*******************************************************************\
Module: Source Lines
Author: Mark R. Tuttle
\*******************************************************************/
/// \file
/// Set of source code lines contributing to a basic block
#include "source_lines.h"
#include <util/format_number_range.h>
#include <util/range.h>
#include <util/source_location.h>
#include <util/string2int.h>
#include <util/string_utils.h>
#include <sstream>
void source_linest::insert(const source_locationt &loc)
{
if(loc.get_file().empty() || loc.is_built_in())
return;
const std::string &file = id2string(loc.get_file());
// the function of a source location can fail to be set
const std::string &func = id2string(loc.get_function());
if(loc.get_line().empty())
return;
std::size_t line = safe_string2size_t(id2string(loc.get_line()));
block_lines[file + ":" + func].insert(line);
}
std::string source_linest::to_string() const
{
std::stringstream ss;
const auto map =
make_range(block_lines).map([&](const block_linest::value_type &pair) {
std::vector<unsigned> line_numbers(
pair.second.begin(), pair.second.end());
return pair.first + ':' + format_number_range(line_numbers);
});
join_strings(ss, map.begin(), map.end(), "; ");
return ss.str();
}

60
src/goto-instrument/source_lines.h Normal file
View File

@ -0,0 +1,60 @@
/*******************************************************************\
Module: Source Lines
Author: Mark R. Tuttle
\*******************************************************************/
/// \file
/// Set of source code lines contributing to a basic block
/// Existing code coverage instrumentation represents the lines of
/// source code contributing to a basic block as a set of line numbers
/// assuming the lines all come from the same source file. In fact,
/// the lines contributing to a basic block can come from multiple
/// files due to function inlining, header file inclusion, etc. This
/// module represents a line of source code with the file, the
/// function, and the line number of the line.
#ifndef CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
#define CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
#include <map>
#include <set>
class source_locationt;
class source_linest
{
public:
/// Constructors
source_linest() = default;
explicit source_linest(const source_locationt &loc)
{
insert(loc);
}
/// Insert a line (a source location) into the set of lines.
/// \param loc: A source location
void insert(const source_locationt &loc);
/// Construct a string representing the set of lines
///
/// \return The set of lines represented as string of the form
/// set1;set2;set3 where each seti is a string of the form
/// file:function:n1,n2,n3,n4 where n1, n2, n3, n4 are line
/// numbers from the given function in the given file listed in
/// ascending order.
std::string to_string() const;
private:
/// A set of lines from a single file
typedef std::set<std::size_t> linest;
/// A set of lines from multiple files
typedef std::map<std::string, linest> block_linest;
block_linest block_lines;
};
#endif // CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H

1
src/util/irep_ids.def
View File

@ -642,6 +642,7 @@ IREP_ID_ONE(cprover_string_to_upper_case_func)
IREP_ID_ONE(cprover_string_trim_func)
IREP_ID_ONE(skip_initialize)
IREP_ID_ONE(basic_block_covered_lines)
IREP_ID_ONE(basic_block_source_lines)
IREP_ID_ONE(is_nondet_nullable)
IREP_ID_ONE(array_replace)
IREP_ID_ONE(switch_case_number)

10
src/util/source_location.h
View File

@ -89,6 +89,11 @@ public:
return get(ID_basic_block_covered_lines);
}
const irep_idt &get_basic_block_source_lines() const
{
return get(ID_basic_block_source_lines);
}
void set_file(const irep_idt &file)
{
set(ID_file, file);
@ -155,6 +160,11 @@ public:
return set(ID_basic_block_covered_lines, covered_lines);
}
void set_basic_block_source_lines(const irep_idt &source_lines)
{
return set(ID_basic_block_source_lines, source_lines);
}
void set_hide()
{
set(ID_hide, true);

1
unit/Makefile
View File

@ -101,6 +101,7 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
../src/cbmc/cbmc_parse_options$(OBJEXT) \
../src/cbmc/fault_localization$(OBJEXT) \
../src/cbmc/xml_interface$(OBJEXT) \
../src/goto-instrument/source_lines$(OBJEXT) \
../src/goto-instrument/cover$(OBJEXT) \
../src/goto-instrument/cover_basic_blocks$(OBJEXT) \
../src/goto-instrument/cover_filter$(OBJEXT) \