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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
module SELF =
struct
type t = {
loc : Filepath.position ;
severe : bool ;
source : string ;
reason : string ;
effect : string ;
}
let compare w1 w2 =
if w1 == w2 then 0 else
let f1 = w1.loc.Filepath.pos_path in
let f2 = w2.loc.Filepath.pos_path in
let fc = Datatype.Filepath.compare f1 f2 in
if fc <> 0 then fc else
let l1 = w1.loc.Filepath.pos_lnum in
let l2 = w2.loc.Filepath.pos_lnum in
let lc = l1 - l2 in
if lc <> 0 then lc else
match w1.severe , w2.severe with
| true , false -> (-1)
| false , true -> 1
| _ -> Stdlib.compare w1 w2
end
include SELF
module Map = Map.Make(SELF)
module Set = Set.Make(SELF)
let severe s = Set.exists (fun w -> w.severe) s
let pretty fmt w =
begin
Format.fprintf fmt
"@[<v 0>%a: warning from %s:@\n"
Cil_datatype.Position.pretty w.loc
w.source ;
if w.severe then
Format.fprintf fmt " - Warning: %s, looking for context inconsistency"
w.effect
else
Format.fprintf fmt " - Warning: %s" w.effect ;
Format.fprintf fmt "@\n Reason: %s@]" w.reason ;
end
type collector = {
default : string ;
mutable warnings : Set.t ;
}
let collector : collector Context.value = Context.create "Warning"
let default () = (Context.get collector).default
exception Error of string * string
let error ?(source="wp") text =
let buffer = Buffer.create 120 in
Format.kfprintf
(fun fmt ->
Format.pp_print_flush fmt () ;
let text = Buffer.contents buffer in
if Context.defined collector then
raise (Error (source,text))
else
Wp_parameters.abort ~current:true "%s" text
) (Format.formatter_of_buffer buffer) text
type context = collector option
let context ?(source="wp") () =
Context.push collector { default = source ; warnings = Set.empty }
let flush old =
let c = Context.get collector in
Context.pop collector old ; c.warnings
let add w =
let c = Context.get collector in
c.warnings <- Set.add w c.warnings
let kprintf phi ?(log=true) ?(severe=false) ?source ~effect message =
let source = match source with Some s -> s | None -> default () in
let buffer = Buffer.create 80 in
Format.kfprintf
(fun fmt ->
Format.pp_print_flush fmt () ;
let text = Buffer.contents buffer in
let loc = Cil_const.CurrentLoc.get () in
if log then
Wp_parameters.warning ~source:(fst loc) "%s" text ~once:true ;
phi {
loc = fst loc ;
severe = severe ;
source = source ;
effect = effect ;
reason = text ;
})
(Format.formatter_of_buffer buffer)
message
let create ?log ?severe ?source ~effect msg =
kprintf (fun w -> w) ?log ?severe ?source ~effect msg
let emit ?severe ?source ~effect msg =
kprintf add ~log:true ?severe ?source ~effect msg
let handle ?(severe=false) ~effect ~handler cc x =
try cc x
with Error(source,reason) ->
if Context.defined collector then
( emit ~severe ~source ~effect "%s" reason ; handler x )
else
if source <> "wp" then
Wp_parameters.fatal ~current:true "[%s] %s" source reason
else
Wp_parameters.fatal ~current:true "%s" reason
type 'a outcome =
| Result of Set.t * 'a
| Failed of Set.t
let catch ?source ?(severe=true) ~effect cc x =
let wrn = context ?source () in
try let y = cc x in Result(flush wrn,y)
with Error(source,reason) ->
emit ~severe ~source ~effect "%s" reason ;
Failed (flush wrn)