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. ## Attachments - [t.c](/uploads/1a30c85b57978846be271f704f121468/t.c)