Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

- Relationships

-  Notes
(0001557)
virgile (developer)
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 (manager)
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
Date Modified Username Field Change
2011-03-04 16:58 signoles New Issue
2011-03-04 16:58 signoles Status new => assigned
2011-03-04 16:58 signoles Assigned To => virgile
2011-03-04 17:09 svn Checkin
2011-03-08 10:12 signoles Description Updated
2011-03-08 10:33 virgile Note Added: 0001557
2011-03-08 10:34 virgile Status assigned => acknowledged
2011-03-08 11:08 signoles Note Added: 0001561
2011-03-08 11:14 svn Checkin
2011-03-08 11:28 svn Checkin
2011-03-10 16:39 svn Checkin
2011-03-10 16:39 svn Status acknowledged => resolved
2011-03-10 16:39 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004824
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker