ID0002217: **This issue was created automatically from Mantis Issue 2217. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002217 | Frama-C | Kernel | public | 2016-03-17 | 2016-06-21 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Ian | **Assigned To** | virgile | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | Ubuntu | **OS Version** | - | | **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium | ### Description : When assigning a range, no error is produced when referencing a formal parameter. ### Steps To Reproduce : test.c: typedef struct obj { char buf[5]; } obj; /*@ assigns x.buf[0..0]; */ void foo(obj x); void bar() { obj tmp; foo(tmp); //@ assert \true; } Running as given above produces no error (it should). > frama-c test.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing test.c (with preprocessing) Running the above program with wp causes an error. > frama-c test.c -wp [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing test.c (with preprocessing) [wp] warning: Missing RTE guards test.c:6:[wp] user error: Address of logic value (tmp_0) [kernel] Plug-in wp aborted: invalid user input. Changing the specification of foo to “assigns x.buf[0]” results in the expected error. > frama-c test.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing test.c (with preprocessing) test.c:6:[kernel] user error: can not assign part of a formal parameter: x.buf[0] [kernel] user error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input.