I tried to verify a program with 2-D array and encountered a problem in the assigns clause.
On the sample code, I can prove the assigns clause in the function of init_2D_2.
But, I failed to prove the same assigns clause in the main function.
The main function does nothing but invokes init_2D_2 so I believe the assigns should be correct.
Can anyone show me why frama-c can't prove it?
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>
#define size 5
#define page 10
/*@
requires \valid( arr+(0..(size-1)) );
requires \valid( arr[0 .. (size-1)]+(0..(page-1)) );
assigns arr[0 .. (size-1)][0..(page-1)];
ensures \forall integer a,b; 0<=a<size && 0<=b<page ==> arr[a][b] == -1;
*/
void init_2D_2(int arr[size][page]){
/*@
loop invariant 0 <= i <= size;
loop invariant \forall integer a,b; 0<=a<i && 0<=b<page ==> arr[a][b] == -1;
loop assigns i, arr[0 .. (size-1)][0..(page-1)];
loop variant size - i;
*/
for(int i=0; i<size; i++) {
/*@
loop invariant 0 <= j <= page;
loop invariant \forall integer a,b; 0<=a<i && 0<=b<page ==> arr[a][b] == -1;
loop invariant \forall integer b; 0<=b<j ==> arr[i][b] == -1;
loop assigns j, arr[i][0..(page-1)];
loop variant page - j;
*/
for(int j=0; j<page; j++) {
arr[i][j] = -1;
}
}
}
int arr2_1[size][page];
/*@
requires \valid( arr2_1[0 .. (size-1)]+(0..(page-1)) );
assigns arr2_1[0 .. (size-1)][0 .. (page-1)];
ensures \forall integer a,b; 0<=a<size && 0<=b<page ==> arr2_1[a][b] == -1;
*/
void main(){
init_2D_2(arr2_1);
}
Frama-c result of main function
Frama-c result of init_2D_2 function
$ frama-c -wp -wp-rte test.c
[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function init_2D_2
[rte:annot] annotating function main
[wp] 33 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_main_assigns_normal : Timeout (Qed:10ms) (10s) (cached)
[wp] [Alt-Ergo 2.4.1] Goal typed_main_assigns_exit : Timeout (Qed:18ms) (10s) (cached)
[wp] [Cache] found:12
[wp] Proved goals: 31 / 33
Qed: 21 (0.67ms-21ms-62ms)
Alt-Ergo 2.4.1: 10 (18ms-40ms) (261) (interrupted: 2) (cached: 12)
$ frama-c -wp -wp-rte -wp-auto wp:split test.c
[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function init_2D_2
[rte:annot] annotating function main
[wp] 33 goals scheduled
[wp] [Failed] Goal typed_main_assigns_exit
Alt-Ergo 2.4.1: Timeout (Qed:7ms) (10s) (cached)
Script: Timeout (Qed:3ms) (10s)
[wp] [Failed] Goal typed_main_assigns_normal
Alt-Ergo 2.4.1: Timeout (Qed:7ms) (10s) (cached)
Script: Timeout (Qed:3ms) (10s)
[wp] [Cache] found:14
[wp] Proved goals: 31 / 33
Qed: 21 (0.56ms-18ms-51ms)
Alt-Ergo 2.4.1: 10 (18ms-40ms) (261) (cached: 10)
First of all, please note that the outcome of such a proof attempt is heavily dependent on the provers you are using, as well as the parameters passed to Frama-C, and finally the version of Frama-C itself. It is thus very important that this information is present in your question if you want an accurate answer. Moreover, the screenshots of Frama-C's gui with the bullets representing the status of each proof obligation do not bring much. It would be more useful to provide, as text, the output of WP on the console.
That said, what follows was obtained with Frama-C 25.0 and Alt-Ergo 2.2.0, using as command line frama-c -wp -wp-rte file.c (with file.c containing your code). I have indeed observed the situation you described:
wp] 33 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_main_assigns_exit : Unknown (Qed:4ms)
[wp] [Alt-Ergo 2.2.0] Goal typed_main_assigns_normal : Unknown (Qed:3ms)
[wp] [Cache] updated:12
[wp] Proved goals: 31 / 33
Qed: 21 (0.49ms-11ms-31ms)
Alt-Ergo 2.2.0: 10 (9ms-19ms-33ms) (124) (unknown: 2)
Digging a little bit further, I've found out that activating the wp:split auto-search strategy of WP makes it simplify enough the formulas to let Alt-Ergo manage the rest: with frama-c -wp -wp-rte -wp-auto wp:split file.c, everything is proved:
[wp] 33 goals scheduled
[wp] Proved goals: 33 / 33
Qed: 21 (0.40ms-13ms-48ms)
Script: 2 (9ms-15ms) (30)
Alt-Ergo 2.2.0: 10 (8ms-28ms) (124)
-wp-auto is a command-line option that ask WP to perform a few automated tactics from the interactive proof editor before giving the resulting formula to the prover. These tactics are described in more detail in Sect. 2.2 of WP's User manual, especially Sect. 2.2.6 on strategies.
EDIT As mentioned in your comment, Alt-Ergo 2.4.1 does not seem to succeed on the goals generated with the -wp-auto wp:split option. Another solution is to use multiple automated provers instead of only Alt-Ergo. For that, you have to install other provers (for instance CVC4 and Z3), and ensure that why3 recognizes them by issuing why3 config detect. Then frama-c -wp -wp-rte -wp-prover alt-ergo,cvc4 file.c should succeed (I'm using cvc4 1.8).
Note that while in this example CVC4 alone can discharge everything (you can check that with -wp-prover cvc4, this might not be the case on other cases, even for examples where Alt-Ergo succeeds for every PO. Similarly, here, while the combination of Alt-Ergo and Z3 works, Z3 (I'm using v4.11) alone leaves a PO unproved, this time on loop invariants.
All in all, automated provers failing to discharge a PO are a fact of life, and using a combination of them can somehow alleviate the problem, even though, when things become sufficiently complicated, there's no alternative to an interactive session, either with WP's TIP (see aforementioned Sect. 2.2), or with the Coq proof assistant (option -wp-interactive, described in Sect. 2.3.8 of the manual).