Frama-C Bug Tracking System - Frama-C
View Issue Details
0000961Frama-CKernelpublic2011-09-13 14:502011-10-10 14:14
yakobowski 
virgile 
normalminoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000961: Cil incorrectly cast arguments to switch to int
The 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.
No tags attached.
Issue History
2011-09-13 14:50yakobowskiNew Issue
2011-09-13 14:50yakobowskiStatusnew => assigned
2011-09-13 14:50yakobowskiAssigned To => virgile
2011-09-13 15:00yakobowskiDescription Updated
2011-09-13 15:37yakobowskiNote Added: 0002255
2011-09-13 15:37yakobowskiPriorityhigh => normal
2011-09-13 15:37yakobowskiSeveritymajor => minor
2011-09-29 17:40svnCheckin
2011-09-29 17:42yakobowskiNote Added: 0002341
2011-09-30 20:34yakobowskiNote Added: 0002372
2011-09-30 20:34yakobowskiStatusassigned => resolved
2011-09-30 20:34yakobowskiResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0002255)
yakobowski   
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   
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   
2011-09-30 20:34   
Fixed in revision 15381.