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