Frama-C Bug Tracking System - Frama-C
View Issue Details
0001309Frama-CKernel > ACSL implementationpublic2012-11-19 16:512014-02-12 16:58
signoles 
virgile 
normalminoralways
closedfixed 
 
Frama-C Fluorine-20130401 
0001309: Incorrect typing of term conditional over floats
void 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 : ?
No tags attached.
? test.ml (440) 2012-11-19 16:51
https://bts.frama-c.com/file_download.php?file_id=454&type=bug
Issue History
2012-11-19 16:51signolesNew Issue
2012-11-19 16:51signolesStatusnew => assigned
2012-11-19 16:51signolesAssigned To => virgile
2012-11-19 16:51signolesFile Added: test.ml
2012-11-19 16:52signolesRelationship addedparent of 0001307
2012-11-19 16:53signolesRelationship deletedparent of 0001307
2012-11-19 16:54signolesRelationship addedparent of 0001307
2012-11-19 16:54signolesRelationship deletedparent of 0001307
2012-11-19 16:54signolesRelationship addedchild of 0001307
2012-11-23 17:28svnCheckin
2012-11-23 17:28svnStatusassigned => resolved
2012-11-23 17:28svnResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2014-02-12 16:58Note Added: 0004607
2014-02-12 16:58Statusclosed => resolved

Notes
(0004607)
   
2014-02-12 16:58   
Fix committed to stable/neon branch.