--- layout: fc_discuss_archives title: Message 6 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?



On Mon, Jan 9, 2012 at 10:05 AM, David MENTRE <dmentre at linux-france.org>wrote:

> 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?


Both: when there are thousands of states for any single program point,
they would take up too much space to keep in memory *and* would not
be convenient for the user to read.


> From a user point of view,
> displaying an over-approximation makes it harder to understand the
> result of value analysis.


If you want to see what is propagated through a specific point chosen
in advance of the analysis, insert Frama_C_dump_each(); at that point,
or, in your case, since you know what you want to observe,
Frama_C_show_each_x_y(x,y);
The two arguments are allowed specifically so that you can see
the values of x in relation to the values of y.

Frama-C vaguely follows the old K&R rules for unprototyped functions,
so you may need to prototype the Frama_C_show_each_...() functions
that you use, if you pass it long ints or floating-point numbers.
Avoiding type clashes is also a good reason never to use
the same suffix in any given program.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120109/20c1b26a/attachment.htm>