Setup GNATcov and improve test coverage (#5)

This adds the script coverage.sh to instrument and run
the unit tests to generate a coverage HTML report.

New tests are added to increase code coverage to 100% (MC/DC).

.github/workflows/ci.yml

@@ -25,14 +25,27 @@ jobs:
         with:
           version: 1.2.0
 
-      - name: Build
+      - name: Build library
         run: alr build --validation
 
-      - name: Unit tests
+      - name: Build and run unit tests (instrumented)
+        run: |
+          cd tests
+          alr gnatcov instrument --level=stmt+mcdc --dump-trigger=atexit --projects cobs.gpr
+          alr build -- --src-subdirs=gnatcov-instr --implicit-with=gnatcov_rts_full
+          alr exec -- bin/unit_tests
+          alr gnatcov coverage --annotate=xcov --output-dir gnatcov_out --level=stmt+mcdc --projects cobs.gpr *.srctrace
+
+      - name: Build and run unit tests (non-instrumented)
         run: |
           cd tests
           alr build --validation
-          alr run
+          alr exec -- bin/unit_tests
+
+      - uses: alire-project/gnatcov-to-codecovio-action@main
+        with:
+          fail_ci_if_error: false # Don't fail the workflow if codecov.io failed
+          verbose: true
 
       - name: Proof
         run: |

README.md

@@ -1,6 +1,6 @@
 # Consistent Overhead Byte Stuffing (COBS)
 This repository provides an implementation of a COBS[1] encoder and
-decoder using the SPARK programming language. 
+decoder using the SPARK programming language.
 
 ## License
 All files are licensed under the MIT license.
@@ -55,11 +55,54 @@ is
 
    type My_COBS is new Generic_COBS (Byte       => Unsigned_8,
                                      Index      => Positive,
-                                     Byte_Count => Positive,
+                                     Byte_Count => Natural,
                                      Byte_Array => Byte_Array);
 end Example;
 ```
 
+## Verification
+
+This project takes a "hybrid verification" approach combining formal
+verification and testing.
+
+GNATprove is used to prove absence of run-time errors. At the time of writing
+there are 139 checks that are automatically proved.
+
+The unit tests are used to check that the encoder and decoder produce the
+correct results for a variety of inputs, with 100% MC/DC source coverage.
+
+### Reproducing the results
+
+#### Proof
+
+To run the proofs:
+
+```sh
+cd prove
+alr exec -- gnatprove -P ../cobs
+```
+
+If you want to see only failed checks, then pass `--report=fail` to `gnatprove`.
+
+#### Tests
+
+To run the unit tests:
+```sh
+alr build --verification
+cd tests
+alr build --verification
+alr run
+```
+
+To run the tests and generate a code coverage report:
+```sh
+alr build --verification
+cd tests
+./coverage.sh
+```
+
+The report will be generated in `tests/gnatcov_out/index.html`.
+
 ## References
 
 [1] Consistent Overheady Byte Stuffing

src/generic_cobs.adb

@@ -60,8 +60,6 @@ is
 
             Code       := B;
             Run_Length := Byte_Count (Byte'Pos (B));
-
-            exit when B = Frame_Delimiter;
          end if;
 
          Run_Length := Run_Length - 1;

tests/.gitignore

@@ -2,3 +2,5 @@
 /bin/
 /alire/
 /config/
+*.srctrace
+/gnatcov_out/

tests/alire.toml

@@ -10,7 +10,8 @@ executables = ["unit_tests"]
 
 [[depends-on]]
 aunit = "^22.0.0"
+gnatcov = "^22.0.1"
 cobs = "*"
 
 [[pins]]
-cobs = { path = "../" }
+cobs = { path = "../" }

tests/coverage.sh

@@ -0,0 +1,14 @@
+#!/bin/sh
+
+alr gnatcov instrument --level=stmt+mcdc --dump-trigger=atexit --projects cobs.gpr
+
+alr build -- --src-subdirs=gnatcov-instr --implicit-with=gnatcov_rts_full
+
+alr exec -- bin/unit_tests
+
+alr gnatcov coverage \
+    --annotate=html+ \
+    --output-dir gnatcov_out \
+    --level=stmt+mcdc \
+    --projects cobs.gpr \
+    *.srctrace