Frama-C-discuss mailing list archives

Pascal.CUOQ at cea.fr (CUOQ Pascal) · Wed, 17 Dec 2008 01:27:04 +0100

> By probing some simple plugins like
>'sparecode', I also get that (correct me If I'm wrong) you interact with
>other plugins through 'Db', and what can be called for each plugin is
>registered in kernel/db.ml.

This is precisely right.

> it's how to walk through the source code. I'm
>currently reading gui/design.ml hoping it might put me on the right
>road, but it's not that easy to get into it.

That's probably the wrong entry point. May I suggest that
you write a plug-in that writes its results on stdout first?
Trying to write your first useful plug-in and insert it into the GUI would be 
trying to solve two difficult problems at the same time.

>For now I just humbly would like to make something as simple as this:
>for $i in each statement in the current project:
>      print some useful information about the statement $i
>endfor

One plug-in that does something very much like this is in the
file src/inout/outputs.ml. It computes what is called "imperative outputs"
in the documentation, for a function kf passed at line 108,
using the "AST visitor" provided by the system. The visitor is a class of
which you can inherit and in which one method per syntactic construct
is pre-defined. You re-define the methods for all the constructs
you are interested in and leave the other ones alone.

Here, being interested in the variables that may be written
to at one statement or another,
the plug-in is interested in instructions (method vinst) that happen to
be assignments (and then it does something with the l-value that is
assigned, with a little help from the value analysis
to transform l-values such as "*p" into something less relative).
It is also interested in function calls
because it wants to take into account the locations that are written
to inside a called function, and that's it.

A more sophisticated example is in inputs.ml in the same directory.
As for outputs, this plug-in goes over the statements in a single pass
with help from the AST visitor.

If you need to visit the statements in the order of the control flow graph
and merge data when paths merge and compute fixpoints, the 
Dataflow functor is for you. The simplest example available is in
context.ml in the same directory. It is a good, if perhaps a bit difficult,
exercise to try to understand what it is supposed to do from reading the
code.

Pascal

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

Frama-C-discuss mailing list archives

[Frama-c-discuss] frama-c plugin howto: question from a beginner