Frama-C Bug Tracking System - Frama-C
View Issue Details
0000655Frama-CKernel > ACSL implementationpublic2010-12-25 19:052014-02-12 16:59
evdenis 
virgile 
normalminoralways
closedfixed 
Frama-C Boron-20100401 
Frama-C Nitrogen-20111001 
0000655: using real function ( \max, \min, \abs ) instead of integer one in function contract
/*@ @ ensures \result == \max( a, b ); @ ensures \result != \min( a, b ); @ ensures a == \abs( a ); @*/ unsigned int max( unsigned int a, unsigned int b ) { int i = a > b ? a : b; //@ assert i == \max( a, b ); return i; } Jessie output: uint32 max(uint32 a, uint32 b) behavior default: ensures (C_8 : ((C_9 : (\result == \real_max(a, b))) && ((C_11 : (\result != \real_min(a, b))) && (C_12 : (a == \real_abs(a)))))); I don't know exactly is it a bug or a feature.
No tags attached.
c max.c (233) 2010-12-25 19:05
https://bts.frama-c.com/file_download.php?file_id=146&type=bug
Issue History
2010-12-25 19:05evdenisNew Issue
2010-12-25 19:05evdenisStatusnew => assigned
2010-12-25 19:05evdenisAssigned To => cmarche
2010-12-25 19:05evdenisFile Added: max.c
2010-12-27 12:17virgileNote Added: 0001358
2010-12-27 12:17virgileAssigned Tocmarche => virgile
2010-12-27 12:17virgileStatusassigned => confirmed
2010-12-27 12:17virgileCategoryPlug-in > jessie => Kernel > ACSL implementation
2011-02-01 16:47svnCheckin
2011-02-01 16:47svnStatusconfirmed => resolved
2011-02-01 16:47svnResolutionopen => fixed
2011-02-09 14:36signolesStatusresolved => closed
2011-02-09 14:37signolesFixed in Version => Frama-C Carbon-20110201
2011-02-09 14:52virgileNote Added: 0001471
2011-02-09 14:52virgileStatusclosed => feedback
2011-02-09 14:52virgileResolutionfixed => reopened
2011-02-09 14:52virgileStatusfeedback => confirmed
2011-02-09 15:57signolesFixed in VersionFrama-C Carbon-20110201 =>
2011-02-10 15:14corrensonNote Added: 0001473
2011-05-06 17:26virgileNote Added: 0001850
2011-05-08 18:32svnCheckin
2011-05-08 18:32svnStatusconfirmed => resolved
2011-05-08 18:32svnResolutionreopened => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004795
2014-02-12 16:59Statusclosed => resolved

Notes
(0001358)
virgile   
2010-12-27 12:17   
This is a bug. The problem lies in type-checking the ACSL annotation, not in the Jessie translation itself. It seems to be partially solved in Carbon-beta and svn, but in some cases overloading resolution still chooses real instead of integer.
(0001471)
virgile   
2011-02-09 14:52   
I don't know why this bug was marked as resolved, but this is not the case in Carbon-20110201
(0001473)
correnson   
2011-02-10 15:14   
I made a mistake at commit (655 instead of ...) 655 was not closed immediately, and I thought it is an error in svn+bts synchro ... Sorry !
(0001850)
virgile   
2011-05-06 17:26   
It seems that the first occurrence of \max gets correctly type-checked, but not the later ones.
(0004795)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.