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.