Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

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


- Issue History
Date Modified Username Field Change
2010-01-21 17:19 lalande New Issue
2010-01-21 17:35 signoles Relationship added duplicate of 0000074
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
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker