FramaCovr

FramaCovr turns the JSON coverage reports emitted by the Frama-C metrics plugin into a gcovr compliant JSON report.

The resulting file can then be consumed by gcovr itself in order to produce an HTML report, a SonarQube coverage import file, a Cobertura report, and so on.

Usage

framacovr \
  --framac-metrics-files given-framac-run-metrics-coverage.json \
                         another-framac-run-metrics-coverage.json \
  --source-dirs kernel/src kernel/include \
  --source-root . \
  -o framacovr.json

Then, with gcovr:

mkdir -p coverage-html
gcovr \
  --root . \
  --json-add-tracefile framacovr.json \
  --html-details coverage-html/coverage.html
gcovr \
  --root . \
  --json-add-tracefile framacovr.json \
  --sonarqube coverage.xml
gcovr \
  --root . \
  --json-add-tracefile framacovr.json \
  --txt

Use the same directory for FraMaCovr --source-root and gcovr --root so that gcovr can resolve the source paths written in the JSON report. The --html-details output path also controls where gcovr writes the generated HTML, CSS and per-file pages.

FraMaCovr options

gcovr options used above

How it works

1. Each metrics report is read. The defined-functions node provides the number of calls of every reached symbol, and the entry-points node lists the traversed symbols.
2. Frama-C symbol instances are canonicalised: a _<n> suffix denotes a static instance and a __fc_inline_<n> suffix a static inline one. All the instances of a given function are merged into a single entry, and their call counts are summed.
3. The source directories are walked and parsed with tree-sitter and its C grammar, in order to bind each function name to its implementation file and to its executable source lines.
4. A gcovr JSON document is emitted. A function called at least once is considered covered, and all its executable lines carry its call count. Source paths are reported relatively to --source-root, which defaults to the current working directory.

Limitations

• Frama-C only provides a function level coverage. Line counts are therefore uniform inside a function, and no branch, condition or decision coverage is reported.
• Sources are parsed without being preprocessed. When a function has several variants guarded by #if/#else in the same file, only the first one is reported.
• A static function defined with the same name in several translation units cannot be distinguished from the metrics output. The merged call count is then reported for each implementation.
• Functions reported by Frama-C but implemented outside of the given source directories (libc stubs, builtins, specified-only-functions) are not part of the report. Run with -v to get their number.

Development

The project requires Python 3.11 or newer. Run all quality checks with:

tox

Build the source and wheel distributions with:

python -m build

License

FraMaCovr is distributed under the Apache License 2.0.