Unexpected label Old in pre : ignored annotation
ID0000979: This issue was created automatically from Mantis Issue 979. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000979 | Frama-C | Plug-in > wp | public | 2011-10-05 | 2014-02-12 |
| Reporter | Anne | Assigned To | Anne | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
A precondition using a user predicate is ignored by wp because of an Old label, but there isn't any label in it :
int bound = 0;
//@ predicate Bok{L} (integer n) = 0 <= bound < n;
/*@ behavior ok: assumes x > 0; requires Bok (3); ensures Bok (5); assigns bound; */ int f (int x);
void g (void) { int x = f(3); //@ assert P: bound < 20; }
The command is : frama-c -wp-fct g -wp-prop P bug.c
The precondition : requires Bok{Pre} (3); gives the same error.