Plug-in inout fails to parse clause /*@ assigns s[..]; */
ID0000068: This issue was created automatically from Mantis Issue 68. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000068 | Frama-C | Plug-in > Eva | public | 2009-04-28 | 2014-02-12 |
| Reporter | ddelmas | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Lithium-20081201 | Target Version | Frama-C Boron-20100401 | Fixed in Version | Frama-C Beryllium-20090902 |
Description :
Consider the following example:
//@ assigns s[..]; void F1(char *s);
char T[100];
void F2(int c) { if (c) F1(T); }
Running "frama-c file.c -main F2 -lib-entry -out" yields a parse error.