GitLab

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.