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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(** Defines some types : they are not all used in each model,
but try to have different names when things are different
(eg. pointer vr address)
*)
include "bool.why"
include "integer.why"
include "real.why"
include "arrays.why"
(*----------------------------------------------------------------------------*)
type 'a option
logic None : 'a option
logic Some : 'a -> 'a option
axiom None_neq_Some : forall v:'a. None <> Some(v)
axiom Some_inj : forall x, y:'a. Some(x) = Some(y) -> x=y
(*----------------------------------------------------------------------------*)
(** Integer types :
*)
type 'a gint
type c_bool
type char
type uchar
type schar
type cint
type uint
type short
type ushort
type long
type ulong
type longlong
type ulonglong
type size_t
(*
logic c_bool : int_type
logic char : int_type
logic uchar : int_type
logic schar : int_type
logic cint : int_type
logic uint : int_type
logic short : int_type
logic ushort : int_type
logic long : int_type
logic ulong : int_type
logic longlong : int_type
logic ulonglong : int_type
logic size_t : int_type
*)
(*-------------------------------------*)
(** Integer conversion : *)
logic int_of_gint : 'a gint -> int
logic char_of_int : int -> char gint
logic cint_of_int : int -> cint gint
(*-------------------------------------*)
(** Integer operations : *)
logic neg_gint : 'a gint -> 'a gint
logic add_gint : 'a gint, 'a gint -> 'a gint
logic sub_gint : 'a gint, 'a gint -> 'a gint
logic mul_gint : 'a gint, 'a gint -> 'a gint
logic div_gint : 'a gint, 'a gint -> 'a gint
logic mod_gint : 'a gint, 'a gint -> 'a gint
(*-------------------------------------*)
(** Integer comparison : *)
logic lt_gint_bool : 'a gint, 'a gint -> bool
logic gt_gint_bool : 'a gint, 'a gint -> bool
logic le_gint_bool : 'a gint, 'a gint -> bool
logic ge_gint_bool : 'a gint, 'a gint -> bool
logic eq_gint_bool : 'a gint, 'a gint -> bool
logic neq_gint_bool : 'a gint, 'a gint -> bool
logic lt_gint : 'a gint, 'a gint -> prop
logic gt_gint : 'a gint, 'a gint -> prop
logic le_gint : 'a gint, 'a gint -> prop
logic ge_gint : 'a gint, 'a gint -> prop
(*-------------------------------------*)
(** Integer operations axioms :
here mapped to why integer operations, but we can have a more specific
axiomatic.
*)
axiom ax_neg_gint :
forall x : 'a gint. int_of_gint(neg_gint(x)) = neg_int(int_of_gint(x))
axiom ax_add_gint : forall x, y : 'a gint.
int_of_gint(add_gint(x,y)) = add_int(int_of_gint(x),int_of_gint(y))
axiom ax_sub_gint :
forall x, y : 'a gint. int_of_gint(sub_gint(x,y)) =
sub_int(int_of_gint(x),int_of_gint(y))
axiom ax_mul_gint :
forall x, y : 'a gint. int_of_gint(mul_gint(x,y)) =
mul_int(int_of_gint(x),int_of_gint(y))
axiom ax_div_gint :
forall x, y : 'a gint. int_of_gint(div_gint(x,y)) =
div_int(int_of_gint(x),int_of_gint(y))
axiom ax_mod_gint :
forall x, y : 'a gint. int_of_gint(mod_gint(x,y)) =
mod_int(int_of_gint(x),int_of_gint(y))
axiom ax_lt_gint_bool :
forall x, y : 'a gint. lt_gint_bool(x,y) =
lt_int_bool(int_of_gint(x),int_of_gint(y))
axiom ax_gt_gint_bool :
forall x, y : 'a gint. gt_gint_bool(x,y) =
gt_int_bool(int_of_gint(x),int_of_gint(y))
axiom ax_le_gint_bool :
forall x, y : 'a gint. le_gint_bool(x,y) =
le_int_bool(int_of_gint(x),int_of_gint(y))
axiom ax_ge_gint_bool :
forall x, y : 'a gint. ge_gint_bool(x,y) =
ge_int_bool(int_of_gint(x),int_of_gint(y))
axiom ax_eq_gint_bool :
forall x, y : 'a gint. eq_gint_bool(x,y) =
eq_int_bool(int_of_gint(x),int_of_gint(y))
axiom ax_neq_gint_bool :
forall x, y : 'a gint. neq_gint_bool(x,y) =
neq_int_bool(int_of_gint(x),int_of_gint(y))
axiom ax_le_gint :
forall x, y : 'a gint. le_gint(x,y) <-> le_int(int_of_gint(x),int_of_gint(y))
axiom ax_ge_gint :
forall x, y : 'a gint. ge_gint(x,y) <-> ge_int(int_of_gint(x),int_of_gint(y))
axiom ax_lt_gint :
forall x, y : 'a gint. lt_gint(x,y) <-> lt_int(int_of_gint(x),int_of_gint(y))
axiom ax_gt_gint :
forall x, y : 'a gint. gt_gint(x,y) <-> gt_int(int_of_gint(x),int_of_gint(y))
(*-------------------------------------*)
(** Booleans *)
(*
logic bool_of_cbool : c_bool gint -> bool
logic _true : c_bool gint
axiom acsl_true_is_bool_true : bool_of_cbool (_true) = true
logic _false : c_bool gint
axiom acsl_false_is_bool_false : bool_of_cbool (_false) = false
*)
logic _true : bool
axiom acsl_true_is_bool_true : (_true) = true
logic _false : bool
axiom acsl_false_is_bool_false : (_false) = false
(* boolean expressions used as integers have to be injected,
but we only know that it is 0 iff the bool is false.
We cannot give any value to a true bool. *)
logic int_of_bool : bool -> int
axiom int_of_bool_false : int_of_bool (false) = 0
axiom int_of_bool_true : int_of_bool (true) <> 0
(*----------------------------------------------------------------------------*)
type 'a pointer
(*----------------------------------------------------------------------------*)
|
