Frama-C Prove While Loop with "/*@ ensures"

Question

I am a newbie at Frama-C and I am trying to validate a C code. The code is very basic but somehow I can not validate it.

In summary, I am trying to prove If that function or loop has ever run. For that, I give a variable a value (4) in the beginning. In the function, I change the value to "5", and I try to ensure that the variable 5 at the end.

The Code:

#include <stdio.h>
int x=4;
/*@
ensures x ==5;
*/
int abs(int val){

    int accept=0;
    int count=3;
    /*@
    loop invariant 0 <= count <= \at(count, Pre);
    loop assigns accept,x,count; 
    loop variant count;
    */
    while (count !=0){
        x=5;
        accept =1;
        count--;
    }
    return x;
 }

I give the command to CLI as "frama-c-gui -wp -rte testp4.c" to start frama-c.

As result: Frama-1

But the "*@ ensures x ≡ 5; */" is still unknown.

Is there anyone can help me about this ? If I take "x=5;" to outside of the while loop ( before return) It validates the /*@ ensures x ==5; */

Thanks in advance to everyone who contributed!

I notice that you have `x ≡ 5` in the link, but `x == 5` here. Also `≤` vs `<=`. — Weather Vane, Jun 23 '22 at 13:59
Isn't your `"x=5"` optimized out maybe? Did you compile with `-O0`? — Jardel Lucca, Jun 23 '22 at 14:04
You should add loop invariant that if count is nonzero then x becomes 5. `\at(count, Pre) != 0 => \at(x, Post) == 5` — tstanisl, Jun 23 '22 at 18:16
@tstanisl I tried your answer as: int x=4; /*@ ensures x ==5; */ int abs(int val){ int accept=0; int count=3; /*@ loop invariant \at(count, Pre) != 0 => \at(x, Post) == 5; loop assigns accept,x,count; loop variant count; */ while (count !=0){ x=5; accept =1; count--; } return x; } But the frama-c responds as like below and do not starts frama-c GUI. ""[kernel] user error: Assignment operators not allowed in annotations."" Did I apply or understand something wrong ? — Uğur B, Jun 23 '22 at 18:39
@tstanisl /*@ loop invariant \at(count, Pre) != 0 ==> \at(x, Post) == 5; loop assigns accept,x,count; loop variant count; */ Like this? Frama-c fails as: [kernel] user error: logic label `Post' not found — Uğur B, Jun 23 '22 at 19:09

Ksass'Peuk · Accepted Answer · 2022-06-25T08:47:40.053

Most of the problems here are related to the use of builtin labels. Here are the labels that we need here:

Pre: the state in precondition
Post: the state in postcondition
LoopEntry: the state when starting the loop
Here: the state at the program point where it is used

First things first. I do not known which version of Frama-C you are using but I'd suggest updating ;) . You would have the following error message to prevent a mistake:

[kernel:annot-error] file.c:11: Warning: 
  unbound logic variable count. Ignoring loop annotation

Why? Because you are talking about count in precondition when it does not exist. Note that in old versions of Frama-C, WP might be OK with this because the pre-state and the initialization of local variables was merged in some cases.

What we want is probably something like "the current value of count is somewhere between 0 and the value it had when we started the loop", thus:

loop invariant 0 <= count <= \at(count, LoopEntry);
which is:
loop invariant 0 <= \at(count, Here) <= \at(count, LoopEntry);

Now that we have this (proven) invariant, we want to link the behavior of the loop with the postcondition (currenty, our loop invariant does not say anything about x and WP does not use the body of the loop out of it. That means that we need another invariant that is "when count does not equal to its value when starting the loop, x is 5`".

Thus:

loop invariant count != \at(count, LoopEntry) ==> x == 5 ;

Which allows to have the program entirely proved :) . Final annotated program:

#include <stdio.h>
int x=4;
/*@
  ensures x ==5;
*/
int abs(int val){

  int accept=0;
  int count=3;
  /*@
    loop invariant 0 <= count <= \at(count, LoopEntry);
    loop invariant count != \at(count, LoopEntry) ==> x == 5 ;
    loop assigns accept,x,count; 
    loop variant count;
  */
  while (count !=0){
    x=5;
    accept =1;
    count--;
  }
  return x;
}

Some words about why \at(count, Pre) != 0 ==> \at(x, Post) == 5 (in the comments) does not work:

\at(count, Pre) is the value of count in precondition of the function and \at(count, Post) is the value of count in postcondition of the function. Thus, not what we need here.

thanks for the explanation and the answer. I added two lines as `loop invariant 0 <= \at(count, Here) <= \at(count, LoopEntry);`, and `loop invariant count != \at(count, LoopEntry) ==> x == 5 ;`. When the x=5 in the while loop, all is good and "ensures x==5" is valid. But when I set x=4 in the loop, the ensure is still VALID **but under hypothesis**. This is it? Or does it still needs improving? — Uğur B, Jun 24 '22 at 11:10
If you change your assignment in the loop, the `loop invariant` cannot be proved anymore: `x` is not `5` but `4`. Thus, WP fails to prove it. Then, recall that when WP creates the verification condition for the `ensures`, it does not use the body of the loop, just the `loop invariant`, thus it can prove the property. But, since the `loop invariant` is not proved (and the proof of the `ensures` depends on it), it only says that it is valid provided that someone succeeds in proving the `loop invariant` (which will not happen here). — Ksass'Peuk, Jun 25 '22 at 08:58

Frama-C Prove While Loop with "/*@ ensures"

1 Answers1