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] needing help to write a frama-c plugin

Hello,

On 09/01/2014 09:38 AM, ZILIO Nicolas wrote:
> I?m writing to you as I?m quite in trouble making a home-made plugin
> working. Here is what I would like to do : given a C programm and after
> having called Impact plugin, i would like to print out in a chosen text
> file all the files' name of the statements found impacted by Impact
> plugin, but with no redundancy.

Good! Writing a Frama-C plug-in is a good choice for such a task.

> I was by the fact thinking of that algorithm for this task :
>
> in : name of the file where results should be printed, files of the
> programm,
>
>            statement to be considered subject to change
>
> out : a text file with results
>
> start
>
>    launch value and so impact analysis
>
>    create an empty list for results
>
>    for each statement of the c programm marked as impacted
>
>        get the file's name where is the statement
>
>        if the file's name is not in the list
>
>            add the file's name to the list
>
>        end if
>
>    end for
>
>    print the list of names into the out_file
>
>    print the number of impacted files (ie the length of the list)
>
> end

The algorithm looks ok, but using a list is inefficient for 
searching-and-replacing. You should better consider to use a set 
(functional way) or an hashtable (imperative way). But ok, for a first 
exercice, using list is ok and, with good encapsulation, switching from 
the one to the other should be easy.

> and in order to do so, I started to write a plugin in the same way about
> the CFG plugin in the developer?s guide and you can find the files of my
> plugin attached.

> Nevertheless, I can?t make it working.

Not tried to compile it, but here are some quick comments...

In your code, functions "length", "member" and "get_nth" already exist 
in the OCaml standard library. They are respectively called List.length, 
List.mem and List.nth. See here:

http://caml.inria.fr/pub/docs/manual-ocaml-4.01/libref/List.html

But you should prevent yourself to use List.nth: its complexity is O(n) 
and almost always results into bad coding style and bad performance. For 
instance in your code, you use a familiar C-like pattern with a for-loop 
over a list which results on an unexpected O(n*n*ln(n)) behaviour where 
n is the size of the list. If you rewrite your for-loop into a recursive 
function, you would not use List.nth anymore (neither List.mem) and you 
would get a standard O(n)) behaviour for a search-and-replace algorithm 
over an unsorted list (and you would get O(ln(n)) by using a set and 
O(1) by using an hashtable).

could you so be kind to tell me :
>
> -am I right about the use of frama-c functions here (the
> ?db.impact.compute_pragmas? and ?the x.location?)?

x.location does not exist. To get the location of a statement, the 
better way is to use the function Cil_datatype.Stmt.loc.

I saw in the
> developers?s guide that I may use something similar to
> ?!db.impact.compute_pragmas?, but I don?t understand why as many plugins
> use for exemple ?db.value.is_computed?.

The type of Db.Value.is_computed is "unit -> bool", meaning that it is a 
function taking one argument of type unit and returning a boolean.

The type of Db.Impact.compute_pragmas is "(unit -> Cil_types.stmt list) 
ref", meaning that it is a reference over a function taking one argument 
of type unit and returning a list of statements. Since it is a 
reference, you have to use "!" to access to the underlying function.

> -is the way I use Cil.DoChildren sufficient here? I?m a bit confused on
> how to use it properly.

Your program is syntactically incorrect since the "for-loop" is not 
closed by the "done" keyword. Semicolon ";" is also missing between your 
OCaml statements (in particular before Cil.DoChildren).

> Moreover, because I?m a lot curious, can I find more documentation about
> this phrase written in the developers? guide : ?An interesting exercise
> would be to change the AST so that execution of each instruction is
> logged to a file, and then re-read that file to print in the CFG how
> much time each instruction has been executed?, especially how execution
> time can be registered here for that?

I'm pretty sure that there is unfortunately no more documentation that 
the existing one. But anyone who successfully solved the exercise and 
would like to contribute is welcome: there is a wiki which might be used 
for that purpose :-).

To conclude, here is a general comment: maybe I'm wrong, but you look 
like a beginner in OCaml programming. Frama-C has its own intricacies 
and the main goal of the Plug-in Development Manual is to explain (most 
of) them. However it assumes that the reader is a fluent OCaml 
programmer (see its introduction) and it might be hard to understand the 
whole story if it is not the case. I'm also not convinced that writing a 
Frama-C plug-in is the simplest way to learn OCaml programming (but of 
course it is doable).

Hope this helps,
Julien