Frama-C initialize array to zero specification

Question

I am trying to prove a specification for a C loop that initialize two integer arrays to zero but i cannot verify it.

Here is the code:

int first[26];
int second[26];
int c;
/*@
loop assigns first[0..(c-1)];
loop assigns second[0..(c-1)];
loop assigns c; 
loop invariant 0 <= c <= 26;
loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;
loop invariant \valid(first+(0..25)) && \valid(second+(0..25));
loop variant 26-c;
*/
for(c = 0; c < 26; c++)
{
  first[c] = 0;
  second[c] = 0;
}

I also tried to use the short form int first[26] = {0}; for zero-initializing but it seems that Frama-C doesn't support that form.

I'm using Frama-C Sodium-20150201 with Alt-Ergo prover and it cannot verify the first three invariants of specification, that are

loop invariant 0 <= c <= 26;
loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;

You loop from 0 to 26 exclusive, so 0 <= c < 26 (0 <= c <= 25). — Kninnug
Doesn't it support something like memset? In that case you could simply use memset(first, 0, 26 * sizeof(int)). — abort
@Kninnug See second comment below stackoverflow.com/questions/32144221/… — Pascal Cuoq

David MENTRÉ David MENTRÉ · Accepted Answer · 2015-08-19T12:05:14

You might have an issue with you Frama-C installation, your code verifies perfectly with default setup.

The code I used:

$ cat loop-init.c 
void loop_init(void)
{
  int first[26];
  int second[26];
  int c;
  /*@
    loop assigns first[0..(c-1)];
    loop assigns second[0..(c-1)];
    loop assigns c; 
    loop invariant 0 <= c <= 26;
    loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
    loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;
    loop invariant \valid(first+(0..25)) && \valid(second+(0..25));
    loop variant 26-c;
  */
  for(c = 0; c < 26; c++)
    {
      first[c] = 0;
      second[c] = 0;
    }
}

Everything is proved:

$ frama-c -wp loop-init.c 
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing loop-init.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 14 goals scheduled
[wp] [Qed] Goal typed_loop_init_loop_inv_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_inv_4_preserved : Valid
[wp] [Alt-Ergo] Goal typed_loop_init_loop_inv_preserved : Valid (16ms) (18)
[wp] [Alt-Ergo] Goal typed_loop_init_loop_inv_2_preserved : Valid (28ms) (26)
[wp] [Qed] Goal typed_loop_init_loop_inv_4_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part2 : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part3 : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part4 : Valid
[wp] [Qed] Goal typed_loop_init_loop_term_decrease : Valid
[wp] [Qed] Goal typed_loop_init_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_loop_init_loop_inv_3_preserved : Valid (1.6s) (68)
[wp] Proved goals:   14 / 14
     Qed:            11 
     Alt-Ergo:        3  (16ms-1.6s) (68)

Frama-C initialize array to zero specification

1 Answers