--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Executing a visitor



On 02/09/2012 09:45 AM, Boris Hollas wrote:
> On Thu, 2012-02-09 at 09:35 +0100, Julien Signoles wrote:
>> This message only indicates that you do not specify any C file on the
>> Frama-C command line. It should not be related to your visitor.
>
> I did specify an input file.
>
>> The example provided in the Plug-in Developer Guide is out-of-date and,
>> if I remember correctly, it does not compile anymore with the last
>> version of Frama-C, even if the call to File.create_project_from_visitor
>> should be correct. Thus you probably try something else. What do you
>> exactly try?
>
> I dynamically register the plugin and call
> File.create_project_from_visitor to initialize the visitor. I changed
> the example, it compiles and frama-c -help lists the plugin. This is
> what happens:
>
> $ frama-c -nonzero t.c
> [kernel] warning: no input file.
> [kernel] preprocessing with "gcc -C -E -I. t.c"

The line of your code:

let prj = File.create_project_from_visitor "non zero divisor" (new 
non_zero_divisor)

is wrongly placed. It must not be put at toplevel of your module but 
inside a function. Moreover your plug-in has no 'main' registered in the 
kernel through Db.Main.extend (see the Plug-in Developer Tutorial).

As a consequence, your visitor is run while Frama-C is not fully 
initialised and, in particular, it does not register yet any C file to 
analyse (that explains the warning).

Something like below would be much better (even if I don't check whether 
there are others errors) :

let main () =
   let prj =
     File.create_project_from_visitor
       "non zero divisor"
       (new non_zero_divisor)
   in
   ... (* do eventually something with prj *)

let () = Db.Main.extend main

Hope this helps,
Julien