Frama-c accepts assigning formal parameters when a range is used

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.