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