--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on January 2012 ---
Hello David, On Mon, Jan 9, 2012 at 9:21 AM, David MENTRE <dmentre at linux-france.org>wrote: > int x, y, z; > > void main(int c) > { > x = c ? 0 : 1; > y = x ? 0 : 1; > z = 10 / (x - y); > } > frama-c-gui -val -slevel 2 possible-zero.c > > ... 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. > This falls under paragraph "Propagation of the displayed states", in section "What the value analysis does not provide", page 46 of the manual, although that paragraph is written backwards with respect to your question. If the value analysis provided propagation of the displayed states, then what you observe in the GUI would be guaranteed to have been propagated, and you would have an assertion for the division. As it is, in your example, the GUI shows an over-approximation of what has really been propagated (that is, once x==1 and y==0 and once x==0 and y==1). No alarm was emitted because the propagated states were not dangerous for the division. Your example seems to come from there and I do not really see how I should make it clearer than: "The values available through the graphical and programmatic interfaces do not come from a single propagated state but from the union of several states that the analyzer may have propagated separately. As a consequence, it should not be assumed that the ?state? displayed at a particular program point has been propagated." But your suggestions are welcome. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120109/c2245d3c/attachment.htm>