--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on July 2010 ---
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