--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Controlling the visitor (Plugin)



Hello,

On Thu, Apr 14, 2011 at 4:54 PM, zakaria chihani <uaz11 at yahoo.fr> wrote:

> Go through the function bodies (that we get by the self#current_func
> method), calculate a cost over the regular statements, but when we find a
> call to another function, we have to add the cost of that function too.
>
> So, we end up with a dependency graph (cycles - mutual recursive functions
> - are of course not handled).
> If we have A which calls B, which calls C, and if the visitor goes through
> the functions in that order, we need to tell him " Stop visiting A, go visit
> the callee before the caller"
>

This is what a function call does.

Is there any way we can fix the visit order "manually"?
>

You do not need to fix the order (although you could). Just force the
missing computations when you encounter a call. See how src/inout/outputs.ml,
which uses a visitor, handles the Call(...) case in vinst. Note that this
will be simplified a bit further in the next release (and, for the same
price, you will also get a better treatment of "fake" recursive calls as
they can appear in some programs).

At the next release, watch how src/inout/outputs.ml was modified and do the
same modifications in your plug-in.

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