--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on February 2012 ---
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