Annotations analysis does not find preprocessor macro
ID0000486: This issue was created automatically from Mantis Issue 486. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000486 | Frama-C | Plug-in > jessie | public | 2010-05-18 | 2010-05-21 |
| Reporter | boris | Assigned To | virgile | Resolution | not fixable |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
Description :
The following is correct c-code, but is doesn't verify.
#define BUFF_SIZE 4
/*@ requires \valid(msg+(0..BUFF_SIZE)); ensures msg[BUFF_SIZE] == '\0'; / int setFoo(char msg) { msg[BUFF_SIZE] = '\0'; return 0; }
~/progs/C/frama-c/test$ frama-c -jessie -pp-annot t.c [kernel] preprocessing with "gcc -C -E -I. -dD t.c" t.c:3:[kernel] user error: Error during annotations analysis: unbound logic variable BUFF_SIZE [kernel] user error: skipping file "t.c" that has errors. [kernel] Plugin kernel aborted because of invalid user input(s).
A work-around is to add a space between .. and BUFF_SIZE.