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
open Cil_types
let is_call_to_sync stmt =
match stmt.skind with
| Instr (Call (_, Var vi, _, _))
when vi.vname = "Frama_C_mthread_sync" -> true
| _ -> false
let kinstr_to_source = function
| Kglobal -> None
| Kstmt stmt -> Some (fst (Cil_datatype.Stmt.loc stmt))
let pretty_succs fmt stmt =
(Pretty_utils.pp_list ~sep:" "
(fun fmt s -> Format.fprintf fmt "%d" s.sid)) fmt stmt.succs
type stack_elt = kernel_function * kinstr
module StackElt = struct
include Datatype.Pair(Kernel_function)(Cil_datatype.Kinstr)
let pretty fmt (f, ki) =
Format.fprintf fmt "@[<hov 2>%s%t@]"
(Ast_info.Function.get_name f.fundec)
(fun fmt -> match ki with
| Kstmt stmt ->
let loc = Cil_datatype.Stmt.loc stmt in
Format.fprintf fmt " :: %a" Cil_datatype.Location.pretty loc
| Kglobal -> ()
)
end
type stack = stack_elt list
module Stack = struct
include Datatype.List(StackElt)
let pretty =
Pretty_utils.pp_list ~pre:"@[<hv>" ~sep:" <-@ " ~suf:"@]" StackElt.pretty
module FunAccessVars =
State_builder.Option_ref(Cil_datatype.Kf)
(struct let dependencies = [Ast.self]
let name = "Stack.FunAccessVars"
end)
let fun_access_vars () =
FunAccessVars.memo (fun () -> Cil_datatype.Kf.dummy)
let access_to_var stmt : stack_elt = fun_access_vars (), Kstmt stmt
let is_access_to_var (kf, _) =
Kernel_function.equal kf (fun_access_vars ())
end