2021-01-15 16:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000979Frama-CPlug-in > wppublic2014-02-12 16:59
ReporterAnne 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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

-Relationships
+Relationships

-Notes

~0002378

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.

~0002379

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

~0002380

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.

~0002381

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

~0002382

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

~0002383

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.

~0002384

Anne (reporter)

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

~0002385

virgile (developer)

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

~0002386

Anne (reporter)

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

~0002387

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

~0004727

Anne (reporter)

Fix committed to stable/neon branch.
+Notes

-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