Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000570Frama-CKernel > ACSL implementationpublic2010-08-24 10:492014-02-12 16:55
Reportermonate 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000570: Incorrect typing of annotations
DescriptionThe following code should be accepted by Frama-C:
====
int main(char *data )
{
  //@ assert \pointer_comparable(data, (void *)0);
  return;
}
====
but leads to "failure: Logic_typing.c_cast_to: char * -> void *"
Implicit promotion from char* to void* is legal according to ACSL.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-08-24 10:49 monate New Issue
2010-08-24 10:49 monate Status new => assigned
2010-08-24 10:49 monate Assigned To => virgile
2010-08-31 18:53 svn Checkin
2010-08-31 18:53 svn Status assigned => resolved
2010-08-31 18:53 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker