--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2012 ---
Hello Pascal, 2012/1/9 Pascal Cuoq <pascal.cuoq at gmail.com>: > "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." The manual is clear. I must admit that I not re-reading the whole manual each time a new release is done. Regarding this specific behaviour of Frama-C, I am wondering if this over-approximation is due to technical constraints (e.g. impossible to store a precise result of the analysis for each analysed path) or simply because it is easier to display? From a user point of view, displaying an over-approximation makes it harder to understand the result of value analysis. But as you rightly said in the manual, "nobody's perfect". ;-) Thank you Pascal, Best regards, david