Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Reduce number of Postconditions with assert
  • From: michaelschausten at googlemail.com (Michael Schausten)
  • Date: Mon, 26 Jul 2010 22:25:28 +0200
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