Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000092Frama-CPlug-in > jessiepublic2009-05-20 18:452009-06-19 09:07
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionreopened 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000092: Why error with logic functions returning a pointer
DescriptionThe following code (a stripped down example of the bug reported by Alan Dunn on the mailing list: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001151.html [^]) gives an erroneous Why file when analyzed with

frama-c -jessie-analysis file.c

Either jessie should exit with an appropriate error message, or the why compilation should succeed.

char T;

/*@
  axiomatic foo {
  logic char* foo{L}(integer x) = &T;
}
*/

/*@ predicate strcmp{L}(char *x, char* y) =
  \forall integer i; (\forall integer j; 0<=j<i ==> *(x+j) !=0) ==>
  *(x+i) == *(y+i);
*/
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000197)
virgile (developer)
2009-06-18 17:46

For some reason, the code snippet that reproduces the bug was cut in the description.
For the bug to appear, the foo logic function must be used, e.g. in the following specification of function f:

/*@ ensures strcmp(foo(x),foo(\result)); */
int f(int x) {
  return x++;
}

- Issue History
Date Modified Username Field Change
2009-05-20 18:45 virgile New Issue
2009-05-25 16:20 signoles Status new => assigned
2009-05-25 16:20 signoles Assigned To => cmarche
2009-05-25 16:20 signoles Status assigned => confirmed
2009-06-18 16:56 cmarche Status confirmed => resolved
2009-06-18 16:56 cmarche Resolution open => unable to reproduce
2009-06-18 17:46 virgile Note Added: 0000197
2009-06-18 17:46 virgile Status resolved => feedback
2009-06-18 17:46 virgile Resolution unable to reproduce => reopened
2009-06-19 09:07 cmarche Status feedback => assigned


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker