unknown identifier in contract is not rejected

ID0001783: This issue was created automatically from Mantis Issue 1783. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001783	Frama-Clang	Kernel	public	2014-05-24	2015-02-18

Reporter	jens	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Neon-20140301	Target Version	-	Fixed in Version	-

Description :

I was playing around with operator overloading and found this example, where the contract mentions an unknown identifier "y". Frama-Clang does not complain about it at all.

class A { int x;

public:

/*@
    // y is unknown here and should be rejected
    ensures \result.x == y;
*/
A& operator=(int x)
{
    this->x = x;
    return *this;
}

};

Additional Information :

This refers to the Frama-Clang version obtained by Virgile on 23. May.

Steps To Reproduce :

in acslplusplus go to the directory C++Examples/OperatorOverloading and call make basic_assignment_error1.wp