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
open Lang
open Lang.F
module L = Qed.Logic
let library = "memory"
let ty_fst_arg = function
| Some l :: _ -> l
| _ -> raise Not_found
let f_eqmem = Lang.extern_fp ~library "eqmem"
let f_memcpy = Lang.extern_f ~library ~typecheck:ty_fst_arg "memcpy"
let p_framed = Lang.extern_fp ~coloring:true ~library "framed"
let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst"
let p_scinit = Lang.extern_fp ~coloring:true ~library "scinit"
let t_malloc = L.Array(L.Int,L.Int)
let t_mem t = L.Array(MemAddr.t_addr,t)
let t_init = L.Array(MemAddr.t_addr,L.Bool)
let sconst memory = p_call p_sconst [ memory ]
let scinit memory = p_call p_scinit [ memory ]
let framed memory = p_call p_framed [ memory ]
let r_eqmem = function
| [_;_;_;n] when n = e_zero -> e_true
| [m0;m1;p;n] when n = e_one -> e_eq (e_get m0 p) (e_get m1 p)
| _ -> raise Not_found
let r_get_memcpy es ks =
match es, ks with
| [m;q;m0;q0;n],[p] ->
begin
match MemAddr.is_separated [p;e_one;q;n] with
| L.Yes -> F.e_get m p
| L.No ->
if p == q then
F.e_get m0 q0
else
if q == q0 then
F.e_get m0 p
else
let i = MemAddr.offset p in
let j = MemAddr.offset q in
let q' = MemAddr.shift q0 (F.e_sub i j) in
F.e_get m0 q'
| _ -> raise Not_found
end
| _ -> raise Not_found
let () = Context.register
begin fun () ->
F.set_builtin f_eqmem r_eqmem ;
F.set_builtin_get f_memcpy r_get_memcpy ;
end
let wkey = Wp_parameters.register_warn_category "union"
let unsupported_union ~model (fd : Cil_types.fieldinfo) =
if not fd.fcomp.cstruct then
Wp_parameters.warning ~once:true ~wkey
"Accessing union fields with %s model might be unsound.@\n\
Please refer to WP manual." model