Frama-C: export a plugin API

Anne Frama-C

I am not sure whether this is still needed in recent Frama-C versions since it seems that a feature was added to do that… to check !

Presentation

This idea is to provide the plugin users with a file that gets the plugin commands with the right types so that they are easier to use.

Data Structure to store the commands

type cmd = { fname : string;
		 type_name : string;
		 type_ml : Format.formatter -> unit;
		 help: Format.formatter -> unit; }

let cmds = ref []

let add_cmd fname ftype help
  let type_name = Type.name ftype in
  let type_ml = Type.pp_ml_name ftype Type.Call in
  let help_fmt = format_of_string ("@["^^help^^"@]") in
  let help fmt = Format.fprintf fmt help_fmt in
  let cmd = { fname; type_name; type_ml; help } in
	cmds := cmd :: !cmds

Register the commands

Just redefine a register function to store information at the same time than the command is registered into Frama-C :

let register fname f ftype help
  add_cmd fname ftype help;
  Dynamic.register ~plugin ~journalize:true fname ftype f

Notice that the arguments are quite the same than the original function, except that a help message has been added to be used as a comment in this API file.

The commands must then be registered as usual, for instance :

let my_cmd
  register "my_cmd" my_cmd
    (Datatype.func Datatype.int Datatype.unit)
    "this is command take an integer and returns nothing"

Print the API

Finally, the API can be printed with :

let pretty_api fmt
  let pp cmd
	Format.fprintf fmt "@[<hov 4>(* [val %s :@;%s]@;%t@;*)@]@."
	  cmd.fname cmd.type_name cmd.help ;
	Format.fprintf fmt
	  "@[<hov 4>let %s =@;@[<hov2>Dynamic.get ~plugin:\"%s\" \"%s\"@;%t@]@]@.@."
	  cmd.fname  plugin cmd.fname cmd.type_ml
  in List.iter pp (List.rev !cmds)

and exported with :

let export_api ()
  try
	let filename = (plugin ^ "_" ^ "api.ml") in
	let och = open_out filename in
	let fmt = Format.formatter_of_out_channel och in
	  P.feedback "export %s API in %s" plugin filename;
	  pretty_api fmt;
	close_out och
  with Sys_error msg -> P.warning "cannot open file: %s" msg

Voir aussi :

Table des matières
Tags
Dernières notes