Cil problem about scope in initialization ?
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...