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.
issue