Frama-C Bug Tracking System - Frama-C
View Issue Details
0000744Frama-CKernel > ACSL implementationpublic2011-03-04 16:582014-03-25 14:17
signoles 
virgile 
normalmajorhave not tried
closedfixed 
 
Frama-C Nitrogen-20111001 
0000744: Too much type promotion for terms
on the above example, C typing rules should apply. Thus no logic term should be logic integer. Unfortunately, in the current implementation, all of them are integer. void main(void) { int x = 0, y = 0; long z = 0L; /*@ assert x == y; */ // x and y are promoted to integer; should be promoted to int instead /*@ assert x == z; */ // x and z are promoted to integer. x should be promoted to long instead }
No tags attached.
Issue History
2011-03-04 16:58signolesNew Issue
2011-03-04 16:58signolesStatusnew => assigned
2011-03-04 16:58signolesAssigned To => virgile
2011-03-04 17:09svnCheckin
2011-03-08 10:12signolesDescription Updated
2011-03-08 10:33virgileNote Added: 0001557
2011-03-08 10:34virgileStatusassigned => acknowledged
2011-03-08 11:08signolesNote Added: 0001561
2011-03-08 11:14svnCheckin
2011-03-08 11:28svnCheckin
2011-03-10 16:39svnCheckin
2011-03-10 16:39svnStatusacknowledged => resolved
2011-03-10 16:39svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004824
2014-02-12 16:59Statusclosed => resolved

Notes
(0001557)
virgile   
2011-03-08 10:33   
Agreed for the comparison between x and y as they are both int. For the comparison between x and z, they have distinct type and are both promoted to integer. The user still can cast x to long if ey want to do the comparison at this level.
(0001561)
signoles   
2011-03-08 11:08   
In the same way, in the example below "x" is promoted to integer bug not "(int)z". Quite strange. /*@ assert x == (int) z; */
(0004824)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.