propagation of \result clauses

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

---

Id	Project	Category	View	Due Date	Updated
ID0000381	Frama-C	Plug-in > Eva	public	2010-01-21	2014-02-12

Reporter	lalande	Assigned To	pascal	Resolution	fixed
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090901	Target Version	-	Fixed in Version	Frama-C Boron-20100401

Description :

Hello,

when discovering Frama-C, I tried to specify some clauses on some functions to specify constraints on the return statement. But it seems that the "ensures" clauses that are "unknown" are not propagated after the analysis of the function.

For example:

/*@ensures \result >= 0; @ensures \result <= 10; int fonc() { int y = rand(); return y; }

int main() { u = fonc(); } gives

y in -;- u in -;-

The @assert seems to be propagated, whereas the constraints on \result not.

I got a response of one of the developer that says that this is in the TODO list... Is it right ?

Best regards,

JF Lalande.

Additional Information :

Frama-C Beryllium 2009-09-01