ID0001143: **This issue was created automatically from Mantis Issue 1143. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001143 | Frama-C | Kernel | public | 2012-04-06 | 2012-04-06 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | no change required | | **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : This is about hiding a variable by redefining another one with the same name, and using the first one in the initialization of the second one. This is a stupid example : int main (void) { int x = 0; int y; { int x = x+1; y = x; } return y; } $ frama-c -print toto.c int main(void) { int x; int y; x = 0; { int x_0; x_0 ++; y = x_0; } return (y); } Shouldn't we have: x_0 = x + 1; instead of x_0 ++; ??? It seems that gcc agrees with me...