Code containing consts should be verifiable

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

---

Id	Project	Category	View	Due Date	Updated
ID0000485	Frama-C	Plug-in > jessie	public	2010-05-18	2010-05-18

Reporter	boris	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090902	Target Version	-	Fixed in Version	-

Description :

Jessie should be able to verify code that contains global C-constants as declared with the keyword const.

I consider using consts instead of macros good programming practice.

Additional Information :

// Doesn't verify:

const int size=4;

/*@ requires \valid(msg+(0..size)); / int setFoo(char msg) { msg[size] = '\0'; return 0; }