Markdown Report (MdR)

Overview

Markdown Report, or MdR for short, is meant to provide a summary of the status (valid, invalid, unknown) of ACSL annotations present in the code under analysis. It features a draft mode, which will output a skeleton of a report in the pandoc-markdown format, with some space left for the user to provide additional information about the context of the analysis, such as an explanation about the ACSL specification used for stubbing a function, or the reasons why an alarm emitted byEva is in fact a false alarm and can thus be ignored.

Once the user is satisfied with the text they have provided, the final document can be produced by MdR. Two output formats can be chosen, either Pandoc Markdown, which can then be transformed into more popular formats (pdf, docx, odt, html, …) with the pandoc tool; or SARIF, the Static Analyzer Results Interchange Format, a JSON schema aiming at unifying the output formats of static analyzers.

Usage

MdR is part of the main distribution of Frama-C. It is typically used after a main analysis, e.g. with:

frama-c -eva file.c -then -mdr-gen sarif -mdr-out file.json

Technical Notes

MdR is currently in an early stage of development; notably, its SARIF output is known to be incomplete.