--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Feedback from jessie plugin



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