--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on September 2009 ---
Hello Pierre-Lo?c, Pierre-Lo?c Garoche a ?crit : > I have two or three questions and remarks about the jessie plugin. > > 1. Does the jessie plugin handles the result of the provers, modifying the status of each annotation for example ? > If yes, how to activate this ? If no, is it a short term goal for you (cf. my question on why mailing list today) ? To my knowledge, it is not-so-short term goal. However, be aware that I am not the responsible of the Jessie plug-in. > 2. Since Beryllium, Jessie is now a dynamic plugin, but it lacks of registered functions. > Could you explain me how to know whether the jessie plugin is available (for example by registering an internal state ?). Below is a quite minimal plug-in implemented this feature: ===== j.ml ===== module P = Plugin.Register (struct let name = "j" let shortname = "j" let descr = "test the presence of jessie" end) let jessie_here () = try ignore (Parameters.Dynamic.Bool.get "-jessie"); true with | Type.StringTbl.Unbound_value _ -> false | exn -> P.fatal "unexepected exception: %s" (Printexc.to_string exn) let main () = P.log "Is Jessie here? %b" (jessie_here ()) let () = Db.Main.extend main ================= Just test it with: $ frama-c -load-script j.ml [j] Is Jessie here? true If you wish a more easy way to do this test, please add a feature request on the BTS. > 3. Concerning this plugin, the (almost) only registered function is the analysis computation. But it cannot be done multiple times since the step 8 contains > Sys.chdir jessie_subdir; > without a backward chdir. > > In case of target C files with relative paths, frama-c get messed up at the second call to jessie. That's a bug (or at least a reasonable feature wish). Please open a task on a BTS. Best regards, Julien Signoles -- Researcher-engineer CEA LIST, Software Reliability Lab 91191 Gif-Sur-Yvette Cedex tel:(+33)1.69.08.82.98 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr