Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000961Frama-CKernelpublic2011-09-13 14:502011-10-10 14:14
Reporteryakobowski 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000961: Cil incorrectly cast arguments to switch to int
DescriptionThe argument of a switch construct should not be cast to int (cf. 6.8.4.2.5). The following program gives a reproducible test case.

int main () {
  unsigned int v = 0xAAAAAAAA;
  switch(v) {
  case 0xAAAAAAAA:
    printf("taken\n");
    return 0;
  default:
    printf("not taken\n");
    return 1;
  }
}

Result with frama-c -val (current version, that handles switch)
__retres ? {1}

Compiled by gcc:
./a.out
taken

GCC's output is the correct one.

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002255)
yakobowski (manager)
2011-09-13 15:37

 Commit 15110 fixes the most problematic part of the problem: integral expressions are no longer cast to int, and non-integral ones are now properly rejected. However, some work remains to be done: the expressions on the labels must be cast to the type of the expression.
(0002341)
yakobowski (manager)
2011-09-29 17:42

 Commit 15110 was buggy in that it did not cas expressions that were too small to int. This is now corrected, but the second part of note 2255 still applies.
(0002372)
yakobowski (manager)
2011-09-30 20:34

 Fixed in revision 15381.

- Issue History
Date Modified Username Field Change
2011-09-13 14:50 yakobowski New Issue
2011-09-13 14:50 yakobowski Status new => assigned
2011-09-13 14:50 yakobowski Assigned To => virgile
2011-09-13 15:00 yakobowski Description Updated
2011-09-13 15:37 yakobowski Note Added: 0002255
2011-09-13 15:37 yakobowski Priority high => normal
2011-09-13 15:37 yakobowski Severity major => minor
2011-09-29 17:40 svn Checkin
2011-09-29 17:42 yakobowski Note Added: 0002341
2011-09-30 20:34 yakobowski Note Added: 0002372
2011-09-30 20:34 yakobowski Status assigned => resolved
2011-09-30 20:34 yakobowski 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

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker