r23410: unsound reporting of pre-condition status
ID0001471: This issue was created automatically from Mantis Issue 1471. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001471 | Frama-C | Kernel | public | 2013-08-29 | 2019-07-05 |
| Reporter | pascal | Assigned To | signoles | Resolution | suspended |
| Priority | low | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
Consider the program below. The pre-condition of f() is not true for all calls.
/*@ ensures l <= \result <= u ; */ int Frama_C_interval(int l, int u);
/*@ requires \valid(p+(0..30)); */ void f(char * p) { *(p + Frama_C_interval(0,30)) = 1; }
int x; void (pf)(char) = f;
void g(char *p) { x = 1; pf(p); }
main(){ char t[31]; g(t); g(t+Frama_C_interval(0,1)); }
Yet:
$ frama-c -val t.c -report …
--- Properties of Function 'f'
[ Valid ] Pre-condition (file t.c, line 4) by Call Preconditions.
And frama-c-gui -val t.c similarly shows a green icon for f's contract when the body of f is displayed.