2021-02-24 18:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000744Frama-CKernel > ACSL implementationpublic2014-03-25 14:17
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0001557

virgile (developer)

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)

In the same way, in the example below "x" is promoted to integer bug not "(int)z". Quite strange.

/*@ assert x == (int) z; */

~0004824

Fix committed to stable/neon branch.
+Notes

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