Unclear status for loop invariants in CSV report
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:
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?