Log message when plevel is used in logic needed
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.