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.