--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Reduce number of Postconditions with assert



Hello,

I have a function which gives me a lot of postconditions. The function 
is given two pointers, which are manipulated multiple times depending on 
some bools:

/*@ ensures (*p) >= \old(*p);
  @ ensures (*q) >= \old(*q);
*/
void myFunction(int *p, int *q) {
    if (bool1) {
        // increase *p, *q in some way
    }
    if (bool2) {
        // increase *p, *q in some way
    }
    // ...
    if (bool9) {
       // increase *p, *q in some way
    }
}

Normally, this gives me a lot of postconditions (in this example, 
approximately 2^9), the first one for the case "bool1 is true, bool2-9 
are false", and so on.
However, I know that the "ensures"-part is not only correct in the end, 
but after every "if". Is there a possibility to make use of this, and 
reduce the number of postconditions (maybe with asserts)? I tried it 
like this:

/*@ ensures (*p) >= \old(*p);
  @ ensures (*q) >= \old(*q);
*/
void myFunction(int *p, int *q) {
    if (bool1) {
        // increase *p, *q in some way
    }
    //@ assert (*p) >= \old(*p);
    //@ assert (*q) >= \old(*q);
    if (bool2) {
        // increase *p, *q in some way
    }
    //@ assert (*p) >= \old(*p);
    //@ assert (*q) >= \old(*q);
    // ...
    if (bool9) {
       // increase *p, *q in some way
    }
}

However, when I try to compile the file, I get the following error:
"Error during analysis of annotation: \old undefined in this context"

Is there another way to get rid of these many postconditions (with 
"assert", or in another way)?


Sincerely,
Michael