package frama-c-lannotate

  1. Overview
  2. Docs

Source file l_function.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Ast_const

include Annotators.Register (struct

    let name = "FC"
    let help = "Function Coverage"

    (** A visitor that adds a label at the start of each function's body *)
    let visitor mk_label = object
      inherit Visitor.frama_c_inplace

      method! vfunc dec =
        if  Annotators.shouldInstrumentFun dec.svar then begin
          let label = mk_label (Exp_builder.one()) [] dec.svar.vdecl in
          dec.sbody.bstmts <- label :: dec.sbody.bstmts;
        end;
        Cil.SkipChildren
    end

    let apply f ast =
      Visitor.visitFramacFileSameGlobals (visitor f) ast

  end)


module StringString = struct
  type t = string * string
  let compare = compare
end
module HL = Set.Make(StringString)
let hyperlabels = ref HL.empty

let disjunctions = Hashtbl.create 100

let compute_hl caller_callee =
  let disj =
    String.concat "+" (List.rev (List.map (fun i -> "l" ^ string_of_int i) (Hashtbl.find_all disjunctions caller_callee)))
  in
  Annotators.next_hl() ^ ") <" ^ disj ^ "|; ;>,"

let gen_hyperlabels_callcov = ref (fun () ->
    let data_filename = (Filename.chop_extension (Annotators.get_file_name ())) ^ ".hyperlabels" in
    Options.feedback "write hyperlabel data (to %s)" data_filename;
    let out = open_out_gen [Open_creat; Open_append] 0o644 data_filename in
    output_string out (HL.fold (fun el str -> str ^ (compute_hl el) ^ "\n") !hyperlabels "");
    close_out out)

(** Call Coverage Visitor **)
class visitor mk_label = object(self)
  inherit Visitor.frama_c_inplace

  val mutable fname = ""
  val mutable floc = Cil_datatype.Location.unknown

  method private mk_call v =
    let newStmt = mk_label (Exp_builder.one()) [] floc in
    Hashtbl.add disjunctions (fname,v.vname) (Annotators.getCurrentLabelId());
    hyperlabels := (HL.add (fname,v.vname) !hyperlabels);
    newStmt

  method! vfunc dec =
    if Annotators.shouldInstrumentFun dec.svar then begin
      fname <- dec.svar.vname;
      floc <- dec.svar.vdecl;
      Cil.DoChildren
    end
    else
      Cil.SkipChildren

  method! vstmt_aux stmt =
    begin match stmt.skind with
      | Instr i when not (Utils.is_label i) ->
        begin match i with
          | Call (_,Var v,_,_)
          | Local_init (_,ConsInit(v, _,_),_) ->
            let newStmt = self#mk_call v in
            stmt.skind <- Block (Cil.mkBlock [newStmt; Stmt_builder.mk stmt.skind]);
            Cil.SkipChildren
          | _ -> Cil.DoChildren
        end
      | _ -> Cil.DoChildren
    end

end

(**
   Call coverage annotator
*)
module CallCov = Annotators.Register (struct
    let name = "FCC"
    let help = "Function Call Coverage"
    let apply mk_label file =
      Visitor.visitFramacFileSameGlobals
        (new visitor mk_label :> Visitor.frama_c_visitor) file;
      !gen_hyperlabels_callcov ()
  end)

(** Nop Visitor **)
class nopvisitor = object(_)
  inherit Visitor.frama_c_inplace
end


(**
   Call coverage annotator
*)
module Empty = Annotators.Register (struct
    let name = "Empty"
    let help = "Process file but add no label"
    let apply _ file =
      Visitor.visitFramacFileSameGlobals (new nopvisitor :> Visitor.frama_c_visitor) file
  end)