Cast on funspec not considering typedef
ID0001518: This issue was created automatically from Mantis Issue 1518. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001518 | Frama-C | Kernel | public | 2013-10-25 | 2017-03-14 |
| Reporter | dpariente | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
[STANCE]
The following code:
/* Generated by Frama-C */ struct rr; typedef struct rr rr; struct apf; struct rr { struct apf *of ; }; typedef struct apf apf; struct apf { apf *next ; rr r ; }; /@ requires r->of == ((void *)0); */ static apf *f(rr *r) { apf *__retres; __retres = r->of; return __retres; }
analyzed by: frama-c -no-unicode cast.c -ocode cast2.c -print ; frama-c -no-unicode cast2.c
generates an error: cast2.c:13:[kernel] user error: unexpected token 'apf' [kernel] user error: skipping file "cast2.c" that has errors. [kernel] Frama-C aborted: invalid user input.