diff --git a/jbmc/regression/jdiff/java-properties/test.desc b/jbmc/regression/jdiff/java-properties/test.desc index a2d74f5bfad..a79dbe66ded 100644 --- a/jbmc/regression/jdiff/java-properties/test.desc +++ b/jbmc/regression/jdiff/java-properties/test.desc @@ -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.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)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.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2 \(lines Test.java:java::Test.:\(\)V:6\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3 \(lines Test.java:java::Test.:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4 \(lines Test.java:java::Test.:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5 \(lines Test.java:java::Test.:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6 \(lines Test.java:java::Test.:\(\)V:7\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1 \(lines Test.java:java::Test.:\(\)V:3\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)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 diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index 166b21616cf..d432f0c26bf 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -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) \ diff --git a/jbmc/src/jdiff/Makefile b/jbmc/src/jdiff/Makefile index 5c491d1363b..2bb2c551e10 100644 --- a/jbmc/src/jdiff/Makefile +++ b/jbmc/src/jdiff/Makefile @@ -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) \ diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index eec4574ff5d..6c60e82cb23 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -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) \ diff --git a/regression/cbmc-cover/block-coverage-report1/main.c b/regression/cbmc-cover/block-coverage-report1/main.c new file mode 100644 index 00000000000..3259e939731 --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report1/main.c @@ -0,0 +1,9 @@ +int main() +{ + int x; + + if(x < 0) + return 0; + else + return 1; +} diff --git a/regression/cbmc-cover/block-coverage-report1/test.desc b/regression/cbmc-cover/block-coverage-report1/test.desc new file mode 100644 index 00000000000..3376924df0b --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report1/test.desc @@ -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 +-- diff --git a/regression/cbmc-cover/block-coverage-report2/main.c b/regression/cbmc-cover/block-coverage-report2/main.c new file mode 100644 index 00000000000..77c606e1c7d --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report2/main.c @@ -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; +} diff --git a/regression/cbmc-cover/block-coverage-report2/test.desc b/regression/cbmc-cover/block-coverage-report2/test.desc new file mode 100644 index 00000000000..c43867e951f --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report2/test.desc @@ -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 +-- diff --git a/regression/cbmc-cover/block-coverage-report3/main.c b/regression/cbmc-cover/block-coverage-report3/main.c new file mode 100644 index 00000000000..80d58679334 --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report3/main.c @@ -0,0 +1,8 @@ +void main() +{ + int x = 0; + while(x < 3) + { + x++; + } +} diff --git a/regression/cbmc-cover/block-coverage-report3/test.desc b/regression/cbmc-cover/block-coverage-report3/test.desc new file mode 100644 index 00000000000..56efc33319f --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report3/test.desc @@ -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 +-- diff --git a/regression/cbmc-cover/block-coverage-report4/main.c b/regression/cbmc-cover/block-coverage-report4/main.c new file mode 100644 index 00000000000..80d58679334 --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report4/main.c @@ -0,0 +1,8 @@ +void main() +{ + int x = 0; + while(x < 3) + { + x++; + } +} diff --git a/regression/cbmc-cover/block-coverage-report4/test.desc b/regression/cbmc-cover/block-coverage-report4/test.desc new file mode 100644 index 00000000000..ce8b645718a --- /dev/null +++ b/regression/cbmc-cover/block-coverage-report4/test.desc @@ -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 +-- diff --git a/regression/cbmc-cover/location1/test.desc b/regression/cbmc-cover/location1/test.desc index 1016f7a1aea..23e8f64b4da 100644 --- a/regression/cbmc-cover/location1/test.desc +++ b/regression/cbmc-cover/location1/test.desc @@ -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 diff --git a/regression/cbmc-cover/location11/test.desc b/regression/cbmc-cover/location11/test.desc index 4f3ab61bc51..2378bee4ca5 100644 --- a/regression/cbmc-cover/location11/test.desc +++ b/regression/cbmc-cover/location11/test.desc @@ -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 diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc index 1b3da668761..bac822b042c 100644 --- a/regression/cbmc-cover/location12/test.desc +++ b/regression/cbmc-cover/location12/test.desc @@ -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 diff --git a/regression/cbmc-cover/location13/test.desc b/regression/cbmc-cover/location13/test.desc index 98c255d8bd1..921e523edbd 100644 --- a/regression/cbmc-cover/location13/test.desc +++ b/regression/cbmc-cover/location13/test.desc @@ -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 diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc index 6fb93526b39..d1a744f1a5d 100644 --- a/regression/cbmc-cover/location14/test.desc +++ b/regression/cbmc-cover/location14/test.desc @@ -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 diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc index 6bb9591efe9..2124e50ad44 100644 --- a/regression/cbmc-cover/location15/test.desc +++ b/regression/cbmc-cover/location15/test.desc @@ -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 diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc index ea8414e88b7..74d7080448c 100644 --- a/regression/cbmc-cover/location16/test.desc +++ b/regression/cbmc-cover/location16/test.desc @@ -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 diff --git a/regression/cbmc-cover/simple_assert/test.desc b/regression/cbmc-cover/simple_assert/test.desc index 57c877afe23..d3fac6c4c46 100644 --- a/regression/cbmc-cover/simple_assert/test.desc +++ b/regression/cbmc-cover/simple_assert/test.desc @@ -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. diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 4a8a6931aa7..a8030dbe428 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -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) \ diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 4c0c3afc7e9..2b4ae9e9fea 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -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) \ diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 6067aa4de8a..8dc28944f66 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -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 \ diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index af3d05f9777..0b0f927edc1 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -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,20 +168,47 @@ 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 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()); + } } std::size_t diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 004ead2c6bd..60e17aa2a05 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -18,6 +18,8 @@ Author: Daniel Kroening #include +#include "source_lines.h" + class cover_blocks_baset { public: @@ -107,6 +109,9 @@ class cover_basic_blockst final : public cover_blocks_baset /// the set of lines belonging to this block std::unordered_set 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 @@ class cover_basic_blockst final : public cover_blocks_baset /// 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 continuation_of_block( @@ -134,6 +143,8 @@ class cover_basic_blocks_javat final : public cover_blocks_baset std::vector block_locations; // map java indexes to block indexes std::unordered_map index_to_block; + // map block number to its source lines + std::vector block_source_lines; public: explicit cover_basic_blocks_javat(const goto_programt &_goto_program); diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp index 460eb87b03f..fa229c8cfdd 100644 --- a/src/goto-instrument/cover_instrument_location.cpp +++ b/src/goto-instrument/cover_instrument_location.cpp @@ -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; diff --git a/src/goto-instrument/source_lines.cpp b/src/goto-instrument/source_lines.cpp new file mode 100644 index 00000000000..ac3c713a370 --- /dev/null +++ b/src/goto-instrument/source_lines.cpp @@ -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 +#include +#include +#include +#include + +#include + +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 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(); +} diff --git a/src/goto-instrument/source_lines.h b/src/goto-instrument/source_lines.h new file mode 100644 index 00000000000..de117ba8c1d --- /dev/null +++ b/src/goto-instrument/source_lines.h @@ -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 +#include + +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 linest; + /// A set of lines from multiple files + typedef std::map block_linest; + + block_linest block_lines; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 22427af79ad..c02d9a6935e 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -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) diff --git a/src/util/source_location.h b/src/util/source_location.h index 999a98179e4..2496b76f898 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -89,6 +89,11 @@ class source_locationt:public irept 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 @@ class source_locationt:public irept 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); diff --git a/unit/Makefile b/unit/Makefile index 8c0d818a08b..5a704019a5c 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -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) \