Documentation for Report plug-in is not correct
-
the issue has not yet been reported on Gitlab; -
the issue has not yet been reported on our old BTS (note: the old BTS is deprecated); -
you installed Frama-C as prescribed in the instructions.
Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0 (Titanium)
- Plug-in used: Report
- OS name: macOS
- OS version: 11.1
Steps to reproduce the issue
- I open the Documentation from Frama-C official page: https://frama-c.com/download/frama-c-user-manual.pdf
- Paragraph: 10.3.2 Rules
- I see a JSON there. This JSON is in curly brackets "{ ... }". And there is a "plugin" property.
- I run:
frama-c -report-rules report_rules.json src/main.c -wp -wp-rte -then -report -then -report-classify
with report_rules.json file:
{
"plugin": "wp" ;
["unknown"]: "[a-zA-Z0-9]*_ensures"
}
as it is on the documentation. 4. I got:
[report] report_rules.json:2: User Error: un-recognised token (at ";")
So first I need to change ";" for ",".
- Then I got:
[report] report_rules.json:3: User Error: missing name (at "[")
Then I added square brackets "[ {...} ]" gave another error:
[report] report_rules.json:3: User Error: missing name (at "[")
-
It has problems with "plugin" property also.
-
With lots of experimentation and time lost I got to some version that works:
[
{"unknown": "[a-zA-Z0-9]*_ensures"}
]
Paragraph 10.3.2 Rules of the documentation is not correct in my point of view. It would be great if there is a tested and working example there. This will save user's time. Currently I still don't know how to structure this JSON so it work with all of its features.
Expected behaviour
Documentation to meet actual JSON format.