Frama-C Bug Tracking System - Frama-C
View Issue Details
0000381Frama-CPlug-in > Evapublic2010-01-21 17:192014-02-12 16:56
lalande 
pascal 
normalfeaturealways
closedfixed 
Frama-C Beryllium-20090901 
Frama-C Boron-20100401 
0000381: propagation of \result clauses
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.
Frama-C Beryllium 2009-09-01
No tags attached.
Issue History
2010-01-21 17:19lalandeNew Issue
2010-01-21 17:35signolesRelationship addedduplicate of 0000074
2010-01-21 17:36signolesNote Added: 0000648
2010-01-21 17:36signolesAssigned To => pascal
2010-01-21 17:36signolesStatusnew => assigned
2010-01-21 17:36signolesCategorykernel => plug-in > value analysis
2010-01-21 17:36signolesAdditional Information Updated
2010-02-23 22:49pascalNote Added: 0000712
2010-02-23 22:50pascalNote Edited: 0000712
2010-02-23 22:51pascalStatusassigned => resolved
2010-02-23 22:51pascalFixed in Version => Frama-C Bore
2010-02-23 22:51pascalResolutionopen => fixed
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0000648)
signoles   
2010-01-21 17:36   
See also the today thread on Frama-C discuss : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001759.html.
(0000712)
pascal   
2010-02-23 22:49   
(edited on: 2010-02-23 22:50)
Fixing miscellaneous syntax errors in the example, the development versin now produces: [value] Values for function main: u IN [0..10] Note that you can also write 0 <= u <= 10 ; for the post-condition, it is a tad more concise.