2021-01-18 08:15 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000381Frama-CPlug-in > Evapublic2010-01-21 17:192014-02-12 16:56
Reporterlalande 
Assigned Topascal 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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

-Relationships
+Relationships

-Notes

~0000648

signoles (manager)

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 (reporter)

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.
+Notes

-Issue History
Date Modified Username Field Change
2010-01-21 17:19 lalande New Issue
2010-01-21 17:36 signoles Note Added: 0000648
2010-01-21 17:36 signoles Assigned To => pascal
2010-01-21 17:36 signoles Status new => assigned
2010-01-21 17:36 signoles Category kernel => plug-in > value analysis
2010-01-21 17:36 signoles Additional Information Updated
2010-02-23 22:49 pascal Note Added: 0000712
2010-02-23 22:50 pascal Note Edited: 0000712
2010-02-23 22:51 pascal Status assigned => resolved
2010-02-23 22:51 pascal Fixed in Version => Frama-C Bore
2010-02-23 22:51 pascal Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2013-12-19 01:14 signoles Source_changeset_attached => framac master 00128456
2014-02-12 16:56 signoles Source_changeset_attached => framac stable/neon 00128456
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History