--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Evaluation of an expression?



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