Frama-C problem with macro substitution in annotations

ID0002147: This issue was created automatically from Mantis Issue 2147. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002147	Frama-C	Kernel > ACSL implementation	public	2015-07-16	2015-07-16

Reporter	dcok@grammatech.com	Assigned To	virgile	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Sodium	Target Version	-	Fixed in Version	-

Description :

This piece of code should parse with frama-c, but does not:

#define MACRO 3

void m() { char buf[MACRO+1]; //@ assert \valid(buf+(0..MACRO)); }

Upon execution, frama-c gives back "[kernel] user error: unbound logic variable MACRO in annotation.".

This piece of code, however, executes as it should:

#define MACRO 3

void m() { char buf[MACRO+1]; //@ assert \valid(buf+(0.. MACRO)); }

This code is also okay:

#define MACRO 3

void m() { char buf[MACRO+1]; //@ assert \valid(buf+(0..(MACRO))); }

It seems that frama-c refuses to substitute defines directly after a .. operator.