frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-11-06T08:45:05Zhttps://git.frama-c.com/pub/frama-c/-/issues/2675Unclear status for loop invariants in CSV report2023-11-06T08:45:05ZAdharsh KamathUnclear status for loop invariants in CSV reportThe meaning of the status for each loop invariant in the CSV file output by the report plugin is unclear. The WP plugin manual does not contain any details regarding the same.
What does "Unknown" or "Partially Proven" status mean for a l...The meaning of the status for each loop invariant in the CSV file output by the report plugin is unclear. The WP plugin manual does not contain any details regarding the same.
What does "Unknown" or "Partially Proven" status mean for a loop invariant?
Does "Unknown" mean the following?
> Under the hypothesis that the other invariants are inductive (established and preserved), this invariant could not be proven to be inductive (failed establishment or preservation, or both)
For example, consider the following program:
```c
extern int unknown_int(void);
int main() {
int i, m, n;
int j, k;
n = unknown_int();
i = unknown_int();
m = unknown_int();
if (!( n == i / 32 )) return 0;
/*@
loop invariant i1: 0 <= j <= i / 8;
loop invariant i2: 0 <= j <= m;
loop invariant i3: j * 4 <= i;
loop invariant i4: j <= n * 8;
*/
for (j = 0; (j < i / 8) && (j < m); j++) {
//@ assert( j/4 < n);
}
return 0;
}
```
Invoking Frama-C with the following command, results in a CSV file with the status for each property:
```
frama-c -wp -wp-verbose 100 -wp-debug 100 -wp-timeout 3 -wp-prover=z3,alt-ergo,cvc4 temp.c -then -report -report-csv frama_c_dump_.csv
```
The CSV output file contains the following:
```
directory file line function property kind status property
. temp.c 1 unknown_int assigns clause Unknown assigns \nothing;
. temp.c 1 unknown_int from clause Unknown assigns \result \from \nothing;
. temp.c 13 main loop invariant Unknown 0 ≤ j ≤ i / 8
. temp.c 14 main loop invariant Unknown 0 ≤ j ≤ m
. temp.c 15 main loop invariant Unknown j * 4 ≤ i
. temp.c 16 main loop invariant Partially proven j ≤ n * 8
. temp.c 19 main user assertion Unknown j / 4 < n
```
What does the status "Unknown" assigned to multiple invariants i1, i2, and i3 mean?
More specifically, **what does it mean to have multiple "Unknown" loop invariants?** Is there a formal description of the possible status values and their meanings? If so, could you please point me in that direction?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/53Documentation for Report plug-in is not correct2021-03-29T11:50:09ZvarosiDocumentation for Report plug-in is not correct- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you insta...- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# 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
1. I open the Documentation from Frama-C official page: https://frama-c.com/download/frama-c-user-manual.pdf
2. Paragraph: **10.3.2 Rules**
3. I see a JSON there. This JSON is in curly brackets "{ ... }". And there is a "plugin" property.
4. 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 ",".
5. 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 "[")
5. It has problems with "plugin" property also.
6. 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.