Cil incorrectly cast arguments to switch to int
ID0000961:
**This issue was created automatically from Mantis Issue 961. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000961 | Frama-C | Kernel | public | 2011-09-13 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
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.
issue