Why error with logic functions returning a pointer
ID0000092: This issue was created automatically from Mantis Issue 92. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000092 | Frama-C | Plug-in > jessie | public | 2009-05-20 | 2009-06-19 |
| Reporter | virgile | Assigned To | cmarche | Resolution | reopened |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Lithium-20081201 | Target Version | - | Fixed in Version | - |
Description :
The following code (a stripped down example of the bug reported by Alan Dunn on the mailing list: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001151.html) gives an erroneous Why file when analyzed with
frama-c -jessie-analysis file.c
Either jessie should exit with an appropriate error message, or the why compilation should succeed.
char T;
/@ axiomatic foo { logic char foo{L}(integer x) = &T; } */
/*@ predicate strcmp{L}(char x, char y) = \forall integer i; (\forall integer j; 0<=j<i ==> *(x+j) !=0) ==> *(x+i) == *(y+i); */