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
|
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie atomique et aux nergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
(* Automatique) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version v2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* struct field of type 'f *)
type 'f field
(* union field of type 'f *)
type 'f ufield
(* f1<>f2 cannot be used if f1 and f2 have different types,
so we define [neq_field] *)
logic neq_field : 'f1 field, 'f2 field -> prop
axiom neq_field_sym : forall f1 : 'f1 field. forall f2 : 'f2 field.
neq_field (f1, f2) -> neq_field (f2, f1)
(* acc_field (s, f) ==== s.[.f] *)
logic acc_field : 'a, 'f field -> 'f
(* upd_field (s, f) ==== mu (s, .f -> x) *)
logic upd_field : 'a, 'f field, 'f -> 'a
(* acc_ufield (s, f) ==== s.[.:f] *)
logic acc_ufield : 'a, 'f ufield -> 'f
(* upd_ufield (s, f) ==== mu (s, .:f -> x) *)
logic upd_ufield : 'a, 'f ufield, 'f -> 'a
axiom acc_upd_field : forall s : 'a. forall f : 'f field. forall x : 'f.
acc_field (upd_field (s, f, x), f) = x
axiom acc_upd_ufield : forall s : 'a. forall f : 'f ufield. forall x : 'f.
acc_ufield (upd_ufield (s, f, x), f) = x
axiom acc_upd_field_neq : forall s : 'a.
forall f1 : 'f1 field. forall f2 : 'f2 field. forall x : 'f2.
neq_field (f1, f2) ->
acc_field (upd_field (s, f2, x), f1) = acc_field (s, f1)
(* From 'why' : logic array_length : 'a farray -> int *)
(* acc_index (t, i) ==== t.[.(i)] *)
logic acc_index : 'a farray , int -> 'a
(* acc_index is 'why' [access] function *)
axiom ax_acc_index : forall t:'a farray. forall i:int.
acc_index (t, i) = access (t, i)
(* upd_index (t, i) ==== mu (t, .(i) -> x) *)
logic upd_index : 'a farray , int, 'a -> 'a farray
(* upd_index is 'why' [update] function *)
axiom ax_upd_index : forall t:'a farray. forall i:int. forall v:'a.
upd_index (t, i, v) = update (t, (i), v)
(* axiom access_update *)
(* axiom access_update_neq *)
(* shift_pointer (p, i) ==== p.[#(i)] *)
logic shift_pointer : 'a pointer, int -> 'a pointer
(* shift_field (ps, f) ==== ps.[+f] *)
logic shift_field : 'a (* struct *) pointer, 'f field -> 'f pointer
(* shift_ufield (ps, f) ==== ps.[+:f] *)
logic shift_ufield : 'a (* union *) pointer, 'f ufield -> 'f pointer
(* shift_index (pt, i) ==== pt.[+(i)] *)
logic shift_index : 'a farray pointer, int -> 'a pointer
logic sub_ptr : 'a pointer, 'a pointer -> int
axiom shift_zero : forall p:'a pointer. shift_pointer(p,0) = p
axiom shift_not_zero :
forall p:'a pointer. forall i:int. i<>0 -> shift_pointer (p, i) <> p
axiom shift_neq : forall p:'a pointer. forall i, j:int. i<>j ->
shift_pointer (p, i) <> shift_pointer (p, j)
axiom shift_shift_pointer :
forall p:'a pointer .
forall i,j:int .
shift_pointer(shift_pointer(p,i),j)
= shift_pointer(p, add_int (i,j))
axiom shift_index_shift_pointer :
forall pt:'a farray pointer. forall i,j:int.
shift_pointer(shift_index(pt,i), j)
= shift_index(pt, add_int (i,j))
logic alloc : int, 't pointer -> 't pointer
axiom base_alloc :
forall i:int. forall p:'t pointer. int_base_addr (alloc (i, p)) = i
axiom base_neq : forall p1 : 't pointer. forall p2 : 't pointer.
int_base_addr (p1) <> int_base_addr (p2) -> p1 <> p2
axiom base_shift_pointer : forall p:'a pointer. forall i:int.
int_base_addr (shift_pointer (p, i)) = int_base_addr (p)
axiom base_shift_index : forall p:'a farray pointer. forall i:int.
int_base_addr (shift_index (p, i)) = int_base_addr (p)
axiom base_shift_field : forall p:'a pointer. forall f : 'f field.
int_base_addr (shift_field (p, f)) = int_base_addr (p)
axiom base_shift_ufield : forall p:'a pointer. forall f : 'f ufield.
int_base_addr (shift_ufield (p, f)) = int_base_addr (p)
axiom disj_field : forall ps:'a (* struct *) pointer.
forall f1 : 'f1 field. forall f2 : 'f2 field. neq_field (f1, f2) ->
disj_pointer (shift_field (ps, f1), (shift_field (ps, f2)))
axiom disj_index : forall p:'a farray pointer. forall i1, i2 : int.
i1 <> i2 -> disj_pointer (shift_index (p, i1), (shift_index (p, i2)))
axiom disj_shift : forall p:'a pointer. forall i1, i2 : int.
i1 <> i2 -> disj_pointer (shift_pointer (p, i1), (shift_pointer (p, i2)))
axiom disj_prop_field : forall p1 : 't1 pointer. forall p2 : 't2 pointer.
forall f : 'tf field.
disj_pointer (p1, p2) -> disj_pointer (p1, shift_field (p2, f))
axiom disj_prop_index : forall i : int.
forall p1 : 't1 pointer. forall p2 : 't2 farray pointer.
disj_pointer (p1, p2) -> disj_pointer (p1, shift_index (p2, i))
axiom disj_base :
forall p1 : 't1 pointer. forall p2 : 't2 pointer.
int_base_addr (p1) <> int_base_addr (p2) ->
disj_pointer (p1, p2)
axiom disj_neq :
forall p1 : 'a pointer. forall p2 : 'a pointer.
disj_pointer (p1, p2) -> p1 <> p2
|
