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