Testing intermediate variables in a large file using Frama-c

Question

I am trying to use Frama-c to check some properties of a C function that I have. The function is quite large and there are some intermediate variables that I need to check. (I am following this and this manual)

My program has the following structure:

1. There are 15 return statements spread throughout the program.

2. The variables I need to check are assigned values at several places in the program, depending on the path of the program.

   my_function(){
   intermediate var 1=xx;
   //@assert var 1>some_value;
   intermediate var 2=yy;
   
   return var 4;
   
   intermediate var 1=xx;
   //@assert var 1>some_value;
   return var 4;
   
   intermediate var 2=xx;            
   intermediate var 1=yy;
   //@assert var 1>some_value;
   
   return var 4;
   }
   

Explanation: I need to check certain properties related to var 1, var 2 and var 4. I tried 2 approaches.

1. use assert whenever var 1 is set as above.

Problem with this was that Frama-C checks only the first assert.

2. use annotations in the beginning.

   /*@ requires \valid(var 1);
      ensures var 1 > some_value;
    */
   

In this case, Frama-C returns an error.

Question: How can I check the properties for intermediate problems? Is there a sample program?

*I haven't included my original function as it is very long.

Answer 1

As Virgile has mentioned, your question is not very clear, but I assume you are trying to validate some properties of var1 and var2. This book provides some nice examples and I think the following should help you.

int abs(int val){
    int res;
    if(val < 0){
    //@ assert val < 0 ;
    res = - val;
    //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val;
    } else {
    //@ assert !(val < 0) ;
    res = val;
    //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val;

    }    
    return res;
}

The author has used the concept of Hoare triples in this scenario, where you check (assert) a certain property by asserting its requirements (pre-condition) for a property and check if a property holds after the corresponding statements are executed.

Hope this helps.