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] 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