GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0001921	Frama-Clang	Plug-in > clang	public	2014-09-12	2015-02-17

Reporter	virgile	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

On the following code:

/*@ ensures \result >= x; */ int f(int& x) { return ++x; }

/*@ ensures \result == x; */ int g(int& x) { return x; }

/*@ ensures \result >= x; */ int h(int x) { return x; }

contracts for g and h are correctly parsed, while contract of f produces the following error messages:

tests/specs/ref_spec.cpp:2:23: comparison of incompatible array types tests/specs/ref_spec.cpp:2:23: expecting a term or predicate tests/specs/ref_spec.cpp:2:23: the term is not a predicate