--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on January 2012 ---
Hello, In a course, I would like to illustrate how one can control precision of Frama-C value analysis. I'm using following example: """ int x, y, z; void main(int c) { x = c ? 0 : 1; y = x ? 0 : 1; z = 10 / (x - y); } """ I'm using Frama-C Nitrogen or Carbon (depending of the machine). In both cases, I'm calling Frama-C with: frama-c-gui -val possible-zero.c and frama-c-gui -val -slevel 2 possible-zero.c In the second case, the assertion "(x - y) != 0" is not inserted, which is I wanted. However, if I do "Evalute expression" at "z = ..." for "x - y", I get {-1; 0; 1; }. I would have expected {-1; 1;} as the assertion is not inserted. Any explanation? Best regards, david