Report

Overview

Report is meant to provide a summary of the status (valid, invalid, unknown) of ACSL annotations present on the code under analysis. Such summary can be provided in different formats: plain text, CSV and JSON. For the latter, it is possible to provide a finer classification according to some user-provided rules. This is mainly intended to be used in conjunction with the WP plug-in, and is documented in the Frama-C user manual.

Usage

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

frama-c -wp -wp-rte file.c -then -report

which will output something like

...
[  Valid  ] Instance of 'Pre-condition 'ordered_length'' at call 'lemma_func_count_subset' (file 04-mjrty.c, line 82)

by Wp.typed.

------------------------------------------------------------
--- Status Report Summary
------------------------------------------------------------
136 Completely validated
300 Considered valid
436 Total
------------------------------------------------------------