[WIP] Expand test coverage

.github/workflows/coverage.yaml

@@ -72,3 +72,8 @@ jobs:
           files: build/html/coverage.info
           fail_ci_if_error: true
           verbose: true
+      - name: Coverage gap report
+        if: always()
+        run: |
+          python3 scripts/coverage_report.py --markdown \
+            build/html/coverage.info >> "$GITHUB_STEP_SUMMARY"

doc/cprover-manual/properties.md

@@ -130,6 +130,7 @@ The goto-instrument program supports these checks:
 | `--undefined-shift-check`    |  add range checks for shift distances                |
 | `--nan-check`                |  add floating-point NaN checks                       |
 | `--uninitialized-check`      |  add checks for uninitialized locals (experimental)  |
+| `--race-check`               |  add data race checks for concurrent programs        |
 | `--error-label label`        |  check that given label is unreachable               |
 
 As all of these checks apply across the entire input program, we may wish to

doc/man/goto-instrument.1

@@ -249,7 +249,7 @@ add checks for uninitialized locals (experimental)
 add check that call stack size of non\-inlined functions never exceeds n
 .TP
 \fB\-\-race\-check\fR
-add floating\-point data race checks
+add data race checks for concurrent programs
 .SS "Semantic transformations:"
 .TP
 \fB\-\-nondet\-volatile\fR

regression/CMakeLists.txt

@@ -64,6 +64,7 @@ else()
   add_subdirectory(goto-cl)
 endif()
 add_subdirectory(goto-cc-cbmc)
+add_subdirectory(goto-cc-modes)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-analyzer-simplify)

regression/acceleration/array_safe1/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_safe2/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_safe3/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_safe4/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_unsafe1/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe2/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe3/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe4/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/const_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/diamond_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/functions_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/nested_unsafe1/test.desc

@@ -5,4 +5,8 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.
+The loop accelerator only handles innermost loops. The outer loop
+(while x < 0x0fffffff) contains a nested inner loop (while y < 10),
+so it is skipped by the contains_nested_loops check in accelerate_loop.
+Only the inner loop is accelerated, which is insufficient to reach the
+assertion after the outer loop within the --unwind bound.

regression/acceleration/overflow_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/phases_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/simple_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/simple_unsafe4/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/cbmc/beautify1/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x;
+  if(x > 0)
+    __CPROVER_assert(x < 0, "should fail");
+  return 0;
+}

regression/cbmc/beautify1/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--beautify
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/show-goto-functions-xml1/main.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/cbmc/show-goto-functions-xml1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show-goto-functions --xml-ui
+^EXIT=0$
+^SIGNAL=0$
+<functions>
+<function.*name="main"
+</functions>
+--
+^warning: ignoring

regression/cbmc/show-loops1/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++)
+    ;
+  return 0;
+}

regression/cbmc/show-loops1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-loops
+^EXIT=0$
+^SIGNAL=0$
+Loop main\.0:
+--
+^warning: ignoring

regression/goto-cc-modes/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/modes.sh $<TARGET_FILE:goto-cc>"
+)

regression/goto-cc-modes/Makefile

@@ -0,0 +1,12 @@
+default: tests.log
+
+test:
+	@../test.pl -e -p -c '../goto-cc-modes/modes.sh ../../../src/goto-cc/goto-cc'
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c '../goto-cc-modes/modes.sh ../../../src/goto-cc/goto-cc'
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.obj' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-cc-modes/goto-armcc-help/dummy.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/goto-cc-modes/goto-armcc-help/test.desc

@@ -0,0 +1,8 @@
+CORE
+dummy.c
+goto-armcc --help
+^EXIT=0$
+^SIGNAL=0$
+goto-armcc understands the options of armcc
+--
+^warning: ignoring

regression/goto-cc-modes/goto-as-help/dummy.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/goto-cc-modes/goto-as-help/test.desc

@@ -0,0 +1,8 @@
+CORE
+dummy.c
+goto-as --help
+^EXIT=0$
+^SIGNAL=0$
+goto-as understands the options of as
+--
+^warning: ignoring

regression/goto-cc-modes/goto-cl-compile/main.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/goto-cc-modes/goto-cl-compile/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+goto-cl /c
+^EXIT=0$
+^SIGNAL=0$
+main\.c
+--
+^warning: ignoring

regression/goto-cc-modes/goto-cl-help/dummy.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/goto-cc-modes/goto-cl-help/test.desc

@@ -0,0 +1,8 @@
+CORE
+dummy.c
+goto-cl --help
+^EXIT=0$
+^SIGNAL=0$
+goto-cl understands the options of CL
+--
+^warning: ignoring

regression/goto-cc-modes/goto-cw-help/dummy.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/goto-cc-modes/goto-cw-help/test.desc

@@ -0,0 +1,8 @@
+CORE
+dummy.c
+goto-cw --help
+^EXIT=0$
+^SIGNAL=0$
+goto-cw understands the options of gcc
+--
+^warning: ignoring

regression/goto-cc-modes/goto-link-help/dummy.c

@@ -0,0 +1 @@
+int main() { return 0; }

regression/goto-cc-modes/goto-link-help/test.desc

@@ -0,0 +1,8 @@
+CORE
+dummy.c
+goto-link --help
+^EXIT=0$
+^SIGNAL=0$
+goto-link understands the options of link
+--
+^warning: ignoring

regression/goto-cc-modes/modes.sh

@@ -0,0 +1,20 @@
+#!/bin/bash
+# Test script for goto-cc mode-specific tests.
+# Usage: modes.sh <goto-cc-binary> <mode-name> [args...]
+#
+# test.pl invokes: CMD OPTIONS 'INPUT'
+# So this receives: modes.sh <goto-cc> <mode> [mode-args...] <input-file>
+#
+# Creates a symlink with the mode name and runs it with the remaining args.
+
+GOTO_CC=$1
+shift
+
+MODE=$1
+shift
+
+TMPDIR=$(mktemp -d)
+trap "rm -rf $TMPDIR" EXIT
+
+ln -sf "$(realpath "$GOTO_CC")" "$TMPDIR/$MODE"
+"$TMPDIR/$MODE" "$@"

regression/goto-diff/change-impact1/a.c

@@ -0,0 +1,10 @@
+int helper(int v)
+{
+  return v + 1;
+}
+
+int main()
+{
+  int x = helper(0);
+  return x;
+}

regression/goto-diff/change-impact1/b.c

@@ -0,0 +1,10 @@
+int helper(int v)
+{
+  return v + 2;
+}
+
+int main()
+{
+  int x = helper(0);
+  return x;
+}

regression/goto-diff/change-impact1/test.desc

@@ -0,0 +1,8 @@
+CORE
+a.c
+b.c --change-impact
+^EXIT=0$
+^SIGNAL=0$
+\*\* helper \*\*
+--
+^warning: ignoring

regression/goto-diff/change-impact2/a.c

@@ -0,0 +1,14 @@
+int compute(int v)
+{
+  return v * 2;
+}
+
+int process(int v)
+{
+  return compute(v) + 1;
+}
+
+int main()
+{
+  return process(5);
+}

regression/goto-diff/change-impact2/b.c

@@ -0,0 +1,14 @@
+int compute(int v)
+{
+  return v * 3;
+}
+
+int process(int v)
+{
+  return compute(v) + 1;
+}
+
+int main()
+{
+  return process(5);
+}

regression/goto-diff/change-impact2/test.desc

@@ -0,0 +1,8 @@
+CORE
+a.c
+b.c --forward-impact
+^EXIT=0$
+^SIGNAL=0$
+\*\* compute \*\*
+--
+^warning: ignoring

regression/goto-diff/unified-diff1/a.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+  return 0;
+}
+
+void foo()
+{
+  int y;
+}