Frama-C Bug Tracking System - Frama-C
View Issue Details
0000744Frama-CKernel > ACSL implementationpublic2011-03-04 16:582014-03-25 14:17
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000744: Too much type promotion for terms
Descriptionon 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
}
TagsNo tags attached.
Attached Files

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.

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:09svn
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:14svn
2011-03-08 11:28svn
2011-03-10 16:39svn
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
2013-12-19 01:12Source_changeset_attached => framac master 797078ee
2013-12-19 01:12Source_changeset_attached => framac master 1a21728e
2014-02-12 16:54Source_changeset_attached => framac stable/neon 797078ee
2014-02-12 16:54Source_changeset_attached => framac stable/neon 1a21728e
2014-02-12 16:59Note Added: 0004824
2014-02-12 16:59Statusclosed => resolved
2014-03-25 14:17signolesSource_changeset_attached => e-acsl stable/neon 1c80c5e0