Writting small scripts s the easiest way to get information from Frama-C when it is not directly available.

How to run a script

To run a script within Frama-C:

$ frama-c -load-script script.ml ...

If the script extract information from the results of a long analysis (such as the value analysis of a large application), it is worth saving the project first (with -save projet.fc) and then to load it together with the script:

$ frama-c -load-script script.ml -load projet.fc

Script about functions

This script prints the list of the defined functions that are not syntactically called:

    let main ()
      let do_function f
        let calls = Kernel_function.find_syntactic_callsites f in
        if ((Kernel_function.is_definition f) && (List.length calls = 0)) then
          Format.printf "  %a:\n    fonction %a@."
            Printer.pp_location (Kernel_function.get_location f)
            Kernel_function.pretty f
      in Globals.Functions.iter do_function

    let () = Db.Main.extend main

Script about variables

This script prints the list of the global variables, and if they are defined or only declared:

    let do_var v _init
      Format.printf "Global variable %a (%s)@." Cil_datatype.Varinfo.pretty v
        (if v.Cil_types.vdefined then "defined" else "declared")

    let () = Db.Main.extend (fun () -> Globals.Vars.iter do_var)

Script about statements

This script shows how to use a visitor: they are used to go through all the program and process some selected elements. Here, the method vstmt is redefined to look at the if statements and to determine if the value of the conditions is statically known. Notice that to print information about the conditions, this script uses the results from the value analysis, so Frama-C must be called with the -val option. Otherwise, the if statements are localized only.

    class test_cond = object inherit Visitor.frama_c_inplace
      method vstmt stmt = match stmt.Cil_types.skind with
      | Cil_types.If (exp,_,_,_) ->
	  let msg
	    if not (Db.Value.is_computed ()) then
	      "no value information"
	    else match Db.Value.condition_truth_value stmt with
	      | true, true -> "both branches"
	      | true, false -> "then branch only"
	      | false, true -> "else branch only"
	      | false, false -> "no branch (unreachable)"
	  in
	  let ()
	    Format.printf "@[<hov2>%a:@ condition (%a) : %s@]@."
	      Printer.pp_location (Cil_datatype.Stmt.loc stmt)
	      Printer.pp_exp exp msg
	  in Cil.DoChildren
      | _ -> Cil.DoChildren
    end

    let () = Db.Main.extend
	(fun () -> Visitor.visitFramacFile (new test_cond) (Ast.get ()))

The function Printer.pp_stmt can be used to print a statement, but the default is to also print the annotations attached to the statement. To print only the statement, rather use (Printer.without_annot Printer.pp_stmt).

Script about properties

This script prints the list of the preconditions of the reachable functions, and for each of them, tells whether it is valid according to the value analysis results, or not:

let do_prop p = match p with
  | Property.IPPredicate (Property.PKRequires _,_,_,idp) ->
      let kf = Extlib.the (Property.get_kf p) in
      if !Db.Value.is_called kf then
        let status = match Property_status.get p with
          | Property_status.Best (Property_status.True, _) -> "is valid"
          | _ -> "may NOT be valid"
        in
        Format.printf "%a: in function '%a', requires '%s' %s \n"
          Printer.pp_location (Property.location p)
          Kernel_function.pretty kf
          (String.concat "_" idp.Cil_types.ip_name)
          status
  | _ -> ()

let () = Db.Main.extend (fun () -> Property_status.iter do_prop)

Script about values

This script iters over assignment statements, and for each of them, and for each callstack that reaches to this statement, it prints the new value of the modified lvalue. Of course, this requires to first compute the value analysis results (ie. to use the -val option):

let pretty_lval stmt fmt lval
  if not (Db.Value.is_computed ()) then Format.fprintf fmt "@,no information"
  else
    let kinstr = Cil_types.Kstmt stmt in
    let loc
      !Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval
    in
    match Db.Value.get_stmt_state_callstack ~after:true stmt with
    | None -> Format.fprintf fmt "@,no information"
    | Some h ->
      let pp cs state
         let value = Db.Value.find state loc in
         Format.fprintf fmt "@,%a: %a"
           Value_types.Callstack.pretty cs Db.Value.pretty value
      in Value_types.Callstack.Hashtbl.iter pp h

class pp_set_lval = object inherit Visitor.frama_c_inplace
    method! vstmt_aux stmt = match stmt.Cil_types.skind with
       | Cil_types.Instr (Cil_types.Set (lval, _exp, loc)) ->
         Format.printf "@[<v5>at %a: '%a' after stmt: %a%a@]@."
           Printer.pp_location loc
            Printer.pp_lval lval
           (Printer.without_annot Printer.pp_stmt) stmt
           (pretty_lval stmt) lval;
         Cil.SkipChildren
       | _ -> Cil.DoChildren
  end

let () = Db.Main.extend
    (fun () -> Visitor.visitFramacFile (new pp_set_lval) (Ast.get ()))

Simple Plugin

Beside the scripts, for more complex things, one can write a Frama-C plugin. A very simple one looks like this :

    let plugin = "Test" (* same name than in Makefile *)
    module P = Plugin.Register
		 (struct
		    let name = "Testing plugin"
		    let shortname = "test"
		    let help = "Just to test..."
		  end)
    module Opt = P.False
		   (struct
		      let option_name = "-test-on"
		      let help = ""
		    end)
    let main ()
      if Opt.is_default () then P.result "default value@."
      else P.result "not the default value@."
    let () = Db.Main.extend main

The plugin then have to be compiled with the Makefile :

FRAMAC_SHARE  	:=$(shell frama-c.byte -print-path)
FRAMAC_LIBDIR 	:=$(shell frama-c.byte -print-libpath)
PLUGIN_NAME	= Test
PLUGIN_CMO	= register

include $(FRAMAC_SHARE)/Makefile.dynamic

To be use, either the plugin is installed within the Frama-C framwork with :

make install

This might require some privileges depending on where Frama-C is installed.

An other solution is to give the path of the plugin with the -add-path option.So for instance :

frama-c -add-path . -help

gives the list of the available plugins and should show :

    ...
    Testing plugin      Just to test...;
                        use -test-help for specific options.
    ....

Frama-C: scripts