Frama-C Bug Tracking System - Frama-C
View Issue Details
0002217Frama-CKernelpublic2016-03-17 21:132016-06-21 14:08
Ian 
virgile 
normalminoralways
closedfixed 
Ubuntu
Frama-C Magnesium 
Frama-C Aluminium 
0002217: Frama-c accepts assigning formal parameters when a range is used
When assigning a range, no error is produced when referencing a formal parameter.
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.
No tags attached.
Issue History
2016-03-17 21:13IanNew Issue
2016-03-18 08:24virgileAssigned To => virgile
2016-03-18 08:24virgileStatusnew => assigned
2016-03-22 22:17yakobowskiNote Added: 0006173
2016-03-22 22:17yakobowskiStatusassigned => resolved
2016-03-22 22:17yakobowskiFixed in Version => Frama-C Aluminium
2016-03-22 22:17yakobowskiResolutionopen => fixed
2016-06-21 14:08signolesStatusresolved => closed

Notes
(0006173)
yakobowski   
2016-03-22 22:17   
We have tightened the checks for non-assignable terms, and your programs is now rejected as expected. Thanks for the report.