Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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