Frama-C Bug Tracking System - Frama-C
View Issue Details
0000979Frama-CPlug-in > wppublic2011-10-05 13:532014-02-12 16:59
normalmajorhave not tried
Frama-C Nitrogen-20111001 
0000979: Unexpected label Old in pre : ignored annotation
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.
No tags attached.
Issue History
2011-10-05 13:53AnneNew Issue
2011-10-05 13:53AnneStatusnew => assigned
2011-10-05 13:53AnneAssigned To => correnson
2011-10-06 08:51virgileNote Added: 0002378
2011-10-06 09:29AnneNote Added: 0002379
2011-10-06 10:01virgileNote Added: 0002380
2011-10-06 10:11AnneNote Added: 0002381
2011-10-06 10:32AnneNote Added: 0002382
2011-10-06 10:56virgileNote Added: 0002383
2011-10-06 10:58AnneNote Added: 0002384
2011-10-06 14:52virgileNote Added: 0002385
2011-10-06 17:08AnneNote Added: 0002386
2011-10-06 17:10AnneNote Added: 0002387
2011-10-06 17:18svnCheckin
2011-10-06 17:18svnStatusassigned => resolved
2011-10-06 17:18svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59AnneNote Added: 0004727
2014-02-12 16:59AnneAssigned Tocorrenson => Anne
2014-02-12 16:59AnneStatusclosed => resolved

2011-10-06 08:51   
Technically, there is a label in requires (and ensures): the one that is passed to Bok. The type-checker is smart enough to infer it, so that it can be omitted when writing the formula, but the normal form has it.
2011-10-06 09:29   
Sorry, but I don't understand your answer Virgile... Where does the Old label comes from ? As I said, even if I give the label in : requires Bok{Pre} (3); I get the message and the precondition is ignored...
2011-10-06 10:01   
Since Bok is declared with a label, you must have a label for each application. Frama-C inserts it implicitly for you when the application occurs in a context where there is a privileged label (i.e. a program annotation, where you have the Here label whatever happens, or a global logic annotation that is itself parameterized by a single label). From what you say, WP apparently converts the Here (and also the Pre that you give explicitly) label into Old for its own taste, but this does not come from the kernel.
2011-10-06 10:11   
> this does not come from the kernel. Yes, of course : it probably comes from the WP translation for the user predicate... but I don't know neither how to fix this, nor how to find a workaround :-( I'll try to have a look in WP source code...
2011-10-06 10:32   
> this does not come from the kernel. Sorry, but it seems that it does :-/ When you try : [frama-c -print bug.c] you get : [requires Bok{Old}(3);] even when you have : [requires Bok{Pre} (3);] in the source file...
2011-10-06 10:56   
Oops, that's right. In addition, the printed file is not parsable (Old only exist for ensures and assigns), which is always a bad idea. Note however that in the original case (without label), the inferred label is Here, which is perfectly valid.
2011-10-06 10:58   
That's right. So there must be a problem in both the kernel and WP ;-)
2011-10-06 14:52   
Commit 15548 fixes Kernel issue. It's now entirely WP's fault :-P
2011-10-06 17:08   
Well : it seems that the bug is now entirely fixed ! So it wasn't WP's fault ;-)
2011-10-06 17:10   
Ooops ! I previously removed the 'behavior' in my example, and that is why it seemed to work, but the bug is still there !...
2014-02-12 16:59   
Fix committed to stable/neon branch.