Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001309Frama-CKernel > ACSL implementationpublic2012-11-19 16:512014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001309: Incorrect typing of term conditional over floats
Descriptionvoid foo(int c) {
  float f = 1.0;
  /*@ assert 0.0 <= (c ? f : 2.0); */
}

In this example, both terms f and 2.0 in the conditional must get type Real. That is not the case. You can see that by running the attached script on this file:
frama-c -load-script test.ml test.i
IF ????? float : ?
TagsNo tags attached.
Attached Files? file icon test.ml [^] (440 bytes) 2012-11-19 16:51 [Show Content]

- Relationships

-  Notes
(0004607)

2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-11-19 16:51 signoles New Issue
2012-11-19 16:51 signoles Status new => assigned
2012-11-19 16:51 signoles Assigned To => virgile
2012-11-19 16:51 signoles File Added: test.ml
2012-11-19 16:52 signoles Relationship added parent of 0001307
2012-11-19 16:53 signoles Relationship deleted parent of 0001307
2012-11-19 16:54 signoles Relationship added parent of 0001307
2012-11-19 16:54 signoles Relationship deleted parent of 0001307
2012-11-19 16:54 signoles Relationship added child of 0001307
2012-11-23 17:28 svn Checkin
2012-11-23 17:28 svn Status assigned => resolved
2012-11-23 17:28 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2014-02-12 16:58 Note Added: 0004607
2014-02-12 16:58 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker