Source file l_statement.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
open Cil_types
open Ast_const
let unk_loc = Fileloc.unknown
let get_fundec_loc dec =
let glob = Ast.def_or_last_decl dec.svar in
match glob with
| GFun (_, loc) -> loc
| _ -> unk_loc
(** A visitor that adds a label at the start of each statement
i.e. :
-Start of a function
-Goto/Return
-Each block of a If
-In Loops
-After each C labels
*)
let visitor mk_label = object(self)
inherit Visitor.frama_c_inplace
method! vfunc dec =
if Annotators.shouldInstrumentFun dec.svar then
let l = mk_label (Exp_builder.one()) [] (get_fundec_loc dec) in
Cil.DoChildrenPost (fun res ->
res.sbody.bstmts <- l :: res.sbody.bstmts;
res
)
else
Cil.SkipChildren
method! vstmt_aux stmt =
match stmt.skind with
| Goto (_, loc)
| Return (_, loc) ->
let l = mk_label (Exp_builder.one()) [] loc in
stmt.skind <- Block (Cil.mkBlock [l; Stmt_builder.mk stmt.skind]);
Cil.SkipChildren
| If (e,b1,b2,loc) ->
let l1 = mk_label (Exp_builder.one()) [] loc in
let nb1 = Cil.visitCilBlock (self :> Cil.cilVisitor) b1 in
let l2 = mk_label (Exp_builder.one()) [] loc in
let nb2 = Cil.visitCilBlock (self :> Cil.cilVisitor) b2 in
nb1.bstmts <- l1 :: nb1.bstmts;
nb2.bstmts <- l2 :: nb2.bstmts;
stmt.skind <- (If (e,nb1,nb2,loc));
Cil.SkipChildren
| Loop _ ->
Cil.DoChildrenPost (fun res ->
match res.skind with
| Loop (ca, b, loc, s1, s2) ->
let lb = mk_label (Exp_builder.one()) [] loc in
b.bstmts<- lb :: b.bstmts;
res.skind <- (Loop (ca,b,loc,s1,s2));
res
| _ -> assert false
)
| _ ->
Cil.DoChildrenPost (fun res ->
if res.labels <> [] then begin
let loc =
match List.hd stmt.labels with
| Label (_,l,_)
| Case (_,l)
| Default l -> l
in
let lb = mk_label (Exp_builder.one()) [] loc in
res.skind <-
begin match res.skind with
| Instr(Skip _) -> lb.skind
| _ -> Block (Cil.mkBlock [lb; Stmt_builder.mk res.skind]);
end;
res
end
else
res
)
end
include Annotators.Register (struct
let name = "STMT"
let help = "Statement Coverage"
let apply f ast =
Visitor.visitFramacFileSameGlobals (visitor f) ast
end)