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

[Frama-c-discuss] Cooperation with Splint



Hi,

Disclaimer: I am a Frama-C developer :-)

Hollas Boris (CR/AEY1) a ?crit :
> Can Jessie be instructed to use a symbol other than @ to introduce
> annotations?

I add a third solution to David's quite sensible proposals:

3. Extensible framework solution: use a custom plugin. Here is a full
example working for Beryllium beta1 based on the "hello world" template.

==main.ml==
(** Register the new plug-in "Custom annotation" and provide access to
some plug-in dedicated features. *)
module Self =
   Plugin.Register
     (struct
        let name = "Custom annotation"
        let shortname = "custom-annot"
        let descr = "Set a custom lexical annotation start"
      end)

(** Register the new Frama-C option "-custom-annot". *)
module Opt =
   Self.EmptyString
     (struct
        let option_name = "-custom-annot"
        let descr = " set a custom annotation start char"
        let arg_name = "<char>"
      end)

(** Set the custom annotation char whenever the option is set. *)
let run () =
   if Opt.is_set () then
     begin
       let annot = Opt.get () in
       if String.length annot <> 1 then
         Self.abort "option -custom-annot expects a single character";
       Self.result
	"Setting custom annotation delimiter to %S" (Opt.get ());
       Clexer.annot_char := annot.[0];
	(* I admit this line cannot be guessed from documentation *)
     end

(** Register the function [run] as a main entry point. *)
let () = Db.Main.extend run
=======

==File Makefile==
FRAMAC_SHARE=$(shell frama-c.byte -print-path)
FRAMAC_LIBDIR=$(shell frama-c.byte -print-libpath)
PLUGIN_NAME=Custom_annot
PLUGIN_CMO=main
include $(FRAMAC_SHARE)/Makefile.dynamic
======

If Frama-C is correctly installed, running make then "make install" 
should work.

Next invokation of Frama-C will support the option "-custom-annot' with 
the expected effect.

Tell me if this is working with your installation.

If you are using a < 3.11 version of Ocaml, only the bytecode version 
will work.

Cheers,
-- 
| Benjamin Monate         | mailto:benjamin.monate at cea.fr     |
| Head of Software Safety Lab.  CEA-LIST/DRT/DTSI/SOL/LSL     |