--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] frama-c boron inconsistency with beryllium



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>