ID0001674: **This issue was created automatically from Mantis Issue 1674. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001674 | Frama-C | Plug-in > Eva | public | 2014-03-05 | 2016-07-05 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed | | **Priority** | low | **Severity** | tweak | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Program: extern int Frama_C_entropy_source; /*@ requires \valid(p + (0 .. l-1)); assigns p[0 .. l-1] \from Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; ensures \initialized(p + (0 .. l-1)); */ void mu(char *p, unsigned l); main(){ int a[48], b[53]; mu(&a, sizeof a); mu(&b, sizeof b); } $ frama-c -val ~/t.c Obtained result: ... [value] computing for function mu <- main. Called from /Users/pascal/t.c:12. [value] using specification for function mu /Users/pascal/t.c:3:[value] Function mu: precondition got status valid. [value] Done for function mu [value] computing for function mu <- main. Called from /Users/pascal/t.c:13. [value] Done for function mu [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ====== [value] Values at end of function main: Frama_C_entropy_source ∈ [--..--] a[0..47] ∈ [--..--] b[0..52] ∈ [--..--] or UNINITIALIZED Wished result: Warning: more than 200 locations to reduce. Approximating. See option -plevel.