--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on May 2010 ---
Hello, Kalyan a ?crit : > Hi, > I tried the syntactic_check plugin from frama-c plugin manual, > and it does not seem to work as expected: > > 1. the order of arguments to Visitor.generic_frama_c_visitor () is > different (also in Beryllium) > 2. the frama-c-gui does not show the assertion generated (and added to > the statement); it was > showing up with Beryllium version. > > It would be great if you could let me know of any alternative way for me > to check if the assertion > has been added or not. You're right. This example of the manual is out-of-date. Please find attached an updated version compatible with Frama-C Boron. This file is just the example of the manual: it is **not** a valid Frama-C plug-in since it is not correctly connected to the Frama-C kernel. In order to test it, you have to run the Frama-C GUI on your C file. Then load this file via the item "Compile and run an ocaml script" of the menu entry "Analyses": the assertions are added in the new project "Syntactic check" as expected (use the menu entry "Project" for switching between projects). If you want a valid Frama-C plug-in, just change the last line of the source: let _ = create_syntactic_check_project () by let () = Db.Main.extend (fun () -> ignore (create_syntactic_check_project ())) In this last case, you can just run it by using the Frama-C option -load-script. Also, how to run any user-written plugin along > with already available > plugins like jessie. (As I would like to have a plugin that generates > annotations, and then call > jessie to verify if the annotations/assertions hold). Plug-ins register their API either in the module Db of the Frama-C kernel or via the function Dynamic.register. In the first case, just have a look at the interface of Db in order to know which functions are available. In the second case, there is yet no easy way to know which functions are registered :-(. Please fill a feature request on the Frama-C BTS (http://bts.frama-c.com) if you really need such a feature. Jessie is a dynamic plug-in which uses the module Dynamic in order to register its API. In order to run it from your own plug-in, just call the function Dynamic.get ~plugin:"Jessie" "run_analysis" (Type.func Type.unit Type.unit) of type unit -> unit. For instance, following the example of syntactic_check.ml, you can modify the function create_syntactic_check_project in order to run Jessie on the new project: let create_syntactic_check_project () = let prj = File.create_project_from_visitor "syntactic check" (new non_zero_divisor) in Project.on prj (Dynamic.get ~plugin:"Jessie" "run_analysis" (Type.func Type.unit Type.unit)) (); prj Hope this helps, Julien Signoles -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: syntactic_check.ml Type: text/x-ocaml Taille: 1894 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100510/796ff2b0/attachment.bin>