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
exception Error of string * string
let current = ref "wp"
let set_model m = current := m
let unsupported ?(model= !current) fmt =
let b = Buffer.create 80 in
Buffer.add_string b "unsupported " ;
let kf fmt =
Format.pp_print_flush fmt () ;
raise (Error(model,Buffer.contents b))
in Format.kfprintf kf (Format.formatter_of_buffer b) fmt
let not_yet_implemented ?(model= !current) fmt =
let b = Buffer.create 80 in
let kf fmt =
Format.pp_print_string fmt " not yet implemented" ;
Format.pp_print_flush fmt () ;
raise (Error(model,Buffer.contents b))
in Format.kfprintf kf (Format.formatter_of_buffer b) fmt
open Cil_types
let pp_logic_label fmt label =
match label with
| BuiltinLabel l -> Printer.pp_logic_builtin_label fmt l
| FormalLabel s -> Format.pp_print_string fmt s
| StmtLabel {contents=stmt} ->
Format.pp_print_string fmt
(let rec pickLabel = function
| [] -> Printf.sprintf "__unknown_label_%d" stmt.sid
| Label (l, _, _) :: _ -> l
| _ :: rest -> pickLabel rest
in pickLabel stmt.labels)
let pp_assigns fmt asgns =
match asgns with
| WritesAny -> Format.fprintf fmt "<undef>"
| _ -> Format.fprintf fmt "@[<hov 2>%a@]" (Printer.pp_full_assigns "") asgns
let pp_string_list ?(sep=format_of_string "@ ") ~empty fmt l =
match l with [] -> Format.fprintf fmt "%s" empty
| _ -> Format.fprintf fmt "%a"
(Pretty_utils.pp_list ~sep Format.pp_print_string) l
let name = function
| [] -> ""
| [x] -> x
| x::xs ->
let buffer = Buffer.create 80 in
Buffer.add_string buffer x ;
List.iter
(fun y -> if y <> "" then
( Buffer.add_char buffer '-' ;
Buffer.add_string buffer y )) xs ;
Buffer.contents buffer