Frama-C Bug Tracking System - Frama-C
View Issue Details
0000381Frama-CPlug-in > Evapublic2010-01-21 17:192014-02-12 16:56
Reporterlalande 
Assigned Topascal 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000381: propagation of \result clauses
DescriptionHello,

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 InformationFrama-C Beryllium 2009-09-01
TagsNo tags attached.
Attached Files

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   
(Last edited: 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.


Issue History
2010-01-21 17:19lalandeNew Issue
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
2013-12-19 01:14signolesSource_changeset_attached => framac master 00128456
2014-02-12 16:56signolesSource_changeset_attached => framac stable/neon 00128456
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva