Highlighted text in code part of the GUI does not take into account size of #defined symbols

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

---

Id	Project	Category	View	Due Date	Updated
ID0000035	Frama-C	Plug-in > jessie	public	2009-04-07	2011-04-01

Reporter	virgile	Assigned To	virgile	Resolution	not fixable
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

Hello,

With following code:

#define MAX 5 int c[5] = {0, }; int global = 0;

void main(void) { //@ assert global == 0; //@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0;

return; }

After launching Jessie GUI on it, if one selects assertion 2., the highlighted text in the lower right corner of the GUI does not cover the " 0" characters.

The previous assertion (1.) is correclty highlighted.

I assume this is because the GUI rely on the size of the expression after preprocessor (CPP) pass while it highlights source code as seen before preprocessor pass. [bug 7496 from old bts, reported by David Mentré] In above example, the expand #define "MAX" is "5", only 1 character wide compared to 3 of "MAX", corresponding to the 3-1=2 characters not highlighted.

I have observed similar behaviour on bigger code, when the highlight is not covering the correct expression at all.

Yours, d.