--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2012 ---
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>