Serial conversions in function result (csmith)
ID0000798:
**This issue was created automatically from Mantis Issue 798. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000798 | Frama-C | Plug-in > Eva | public | 2011-04-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **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 :
short x = -10;
int y, z, t;
unsigned short f(void)
{
return x;
}
unsigned short g(void)
{
unsigned short l = *(unsigned short*)&x;
return l;
}
main(){
y = *(unsigned short*)&x;
z = f();
t = g();
}
y and z are computed correctly, but t is wrong:
[value] Values for function main:
y IN {65526; }
z IN {65526; }
t IN {-10; }
issue