Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>