I believe I am missing something obvious, but I have tried a lot and I haven't managed to find the source of the problem.
I am following the acsl guide from Frama-C. There is this introductory example of how to verify the correctness of finding the maximum value in an array:
/*@ requires n > 0;
requires \valid(p+ (0 .. n-1));
ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i];
ensures \exists int e; 0 <= e <= n-1 && \result == p[e];
*/
int max_seq(int* p, int n) {
int res = *p;
for(int i = 0; i < n; i++) {
if (res < *p) { res = *p; }
p++;
}
return res;
}
However, running frama-c -wp -wp-prover alt-ergo samenum.c -then -report I get:
[wp] Warning: Missing RTE guards
[wp] samenum.c:8: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_seq_ensures_2 : Timeout (Qed:1ms) (10s)
[wp] [Alt-Ergo] Goal typed_max_seq_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (interrupted: 2)
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'max_seq'
--------------------------------------------------------------------------------
[ - ] Post-condition (file samenum.c, line 3)
tried with Wp.typed.
[ - ] Post-condition (file samenum.c, line 4)
tried with Wp.typed.
[ - ] Default behavior
tried with Frama-C kernel.
It seems that alt-ergo times out before proving the property. For what is worth, I tried with higher time-out but it still doesn't work.
I am using:
I am running this on Ubuntu 18.04 and before running the command I run: why3 config --detect to make sure why3 knows about alt-ergo.
Any ideas? Can anyone verify that this is example is not working? Any help would be greatly appreciated!
This mini-tutorial was written quite a long time ago and is not really up to date. A new version of the website should appear in the upcoming months. Basically, this contract, as well as the invariant for the loop pointed by @iguerNL were meant to be verified using the Jessie plugin, and not the WP plugin of Frama-C. Among the differences between these two plugins, Jessie did not need assigns clauses for loops and functions, while WP needs them.
Thus, a complete annotated max_seq function could be this one:
/*@ requires n > 0;
requires \valid(p+ (0..n−1));
assigns \nothing;
ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];
ensures \exists int e; 0 <= e <= n−1 && \result == p[e];
*/
int max_seq(int* p, int n) {
int res = *p;
//@ ghost int e = 0;
/*@ loop invariant \forall integer j; 0 <= j < i ==> res >= \at(p[j],Pre);
loop invariant \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res;
loop invariant 0<=i<=n;
loop invariant p==\at(p,Pre)+i;
loop invariant 0<=e<n;
loop assigns i, res, p, e;
loop variant n-i;
*/
for(int i = 0; i < n; i++) {
if (res < *p) {
res = *p;
//@ ghost e = i;
}
p++;
}
return res;
}
where we specify that the functions does not assign anything in memory, and that the loop assigns the different local variables i, res, p and e (thus leaving n unchanged).
Note that more recent tutorials are available to learn about the use of Frama-C with the WP plugin. The future version of the Frama-C website mentions: