--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on June 2014 ---
Hello, I tried to explain how -slevel works at some colleague. I used the attached example. I hope it will help others to get a clearer view on the behaviour of -slevel. Best regards, david -------------- next part -------------- /* Test this program with: frama-c -val -slevel 1 slevel-example.c and frama-c -val -slevel 2 slevel-example.c And look at the value of "x". With -slevel 1 we have "x ??? {2; 3; 4}" and with -slevel 2 with have "x ??? {2; 4}". Why? Because -slevel increases the number of different considered path for the analysis. In our program: -slevel | c | a | g(c,a) | x ------------------------------------------------------------------------------ 1 | c ??? {0; 1} | a ??? {2; 3} | g(c,a) ??? {(0,2); (1,2); | x ??? {2; 3; 4} | | | (0;3); (1,3)} | ------------------------------------------------------------------------------ 2 | | | | |-path 1 | c ??? {0} | a ??? {2} | g(c,a) ??? {(0,2)} | x ??? {2} \-path 2 | c ??? {1} | a ??? {3} | g(c,a) ??? {(1,3)} | x ??? {4} | | | | aggregated| c ??? {0; 1} | a ??? {2; 3} | | x ??? {2; 4} result | I hope result of Frama-C analysis is clearer now. David Mentr??, 19th of June, 2014. */ extern int entropy_source; /*@ assigns \result \from entropy_source; assigns entropy_source \from entropy_source; ensures \result == 0 || \result == 1; */ int f(void); // f() returns indeterministically 0 or 1 int g(int x, int y) { return x + y; } void main(void) { int c; int a = 2; int x; c = f(); if (c) { a = 3; } x = g(c, a); }