2021-01-15 16:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000979Frama-CPlug-in > wppublic2014-02-12 16:59
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityhave not tried
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000979: Unexpected label Old in pre : ignored annotation
DescriptionA 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.
TagsNo tags attached.
Attached Files




virgile (developer)

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.


Anne (reporter)

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...


virgile (developer)

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.


Anne (reporter)

> 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...


Anne (reporter)

> 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...


virgile (developer)

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.


Anne (reporter)

That's right. So there must be a problem in both the kernel and WP ;-)


virgile (developer)

Commit 15548 fixes Kernel issue. It's now entirely WP's fault :-P


Anne (reporter)

Well : it seems that the bug is now entirely fixed ! So it wasn't WP's fault ;-)


Anne (reporter)

Ooops ! I previously removed the 'behavior' in my example, and that is why it seemed to work, but the bug is still there !...


Anne (reporter)

Fix committed to stable/neon branch.

-Issue History
Date Modified Username Field Change
2011-10-05 13:53 Anne New Issue
2011-10-05 13:53 Anne Status new => assigned
2011-10-05 13:53 Anne Assigned To => correnson
2011-10-06 08:51 virgile Note Added: 0002378
2011-10-06 09:29 Anne Note Added: 0002379
2011-10-06 10:01 virgile Note Added: 0002380
2011-10-06 10:11 Anne Note Added: 0002381
2011-10-06 10:32 Anne Note Added: 0002382
2011-10-06 10:56 virgile Note Added: 0002383
2011-10-06 10:58 Anne Note Added: 0002384
2011-10-06 14:52 virgile Note Added: 0002385
2011-10-06 17:08 Anne Note Added: 0002386
2011-10-06 17:10 Anne Note Added: 0002387
2011-10-06 17:18 svn
2011-10-06 17:18 svn Status assigned => resolved
2011-10-06 17:18 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 Anne Source_changeset_attached => framac master cb8e9f81
2014-02-12 16:54 Anne Source_changeset_attached => framac stable/neon cb8e9f81
2014-02-12 16:59 Anne Note Added: 0004727
2014-02-12 16:59 Anne Assigned To correnson => Anne
2014-02-12 16:59 Anne Status closed => resolved
+Issue History