Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / wpdir / typed / toto_step_assert_20_Alt-Ergo.mlw @ 6a93d814

History | View | Annotate | Download (32.6 KB)

1
(**************************************************************************)
2
(*                                                                        *)
3
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
5
(*                                                                        *)
6
(*  This software is distributed under the terms of the GNU Lesser        *)
7
(*  General Public License version 2.1, with the special exception        *)
8
(*  on linking described in file LICENSE.                                 *)
9
(*                                                                        *)
10
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
11
(*                        énergies alternatives).                         *)
12
(*                                                                        *)
13
(**************************************************************************)
14

    
15
(* this is a prelude for Alt-Ergo*)
16
(* this is a prelude for Alt-Ergo integer arithmetic *)
17
(** The theory BuiltIn_ must be appended to this file*)
18
(** The theory Bool_ must be appended to this file*)
19
(**************************************************************************)
20
(*                                                                        *)
21
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
22
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
23
(*                                                                        *)
24
(*  This software is distributed under the terms of the GNU Lesser        *)
25
(*  General Public License version 2.1, with the special exception        *)
26
(*  on linking described in file LICENSE.                                 *)
27
(*                                                                        *)
28
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
29
(*                        énergies alternatives).                         *)
30
(*                                                                        *)
31
(**************************************************************************)
32

    
33
(* this is a prelude for Alt-Ergo*)
34
(** The theory BuiltIn_ must be appended to this file*)
35
(** The theory Bool_ must be appended to this file*)
36
(** The theory int_Int_ must be appended to this file*)
37
logic abs_int : int -> int
38

    
39
axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))
40

    
41
axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))
42

    
43
axiom Abs_le :
44
  (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))
45

    
46
axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))
47

    
48
axiom Abs_le2 :
49
  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
50
  (abs_int(x) <= y)))
51

    
52
axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))
53

    
54
(**************************************************************************)
55
(*                                                                        *)
56
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
57
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
58
(*                                                                        *)
59
(*  This software is distributed under the terms of the GNU Lesser        *)
60
(*  General Public License version 2.1, with the special exception        *)
61
(*  on linking described in file LICENSE.                                 *)
62
(*                                                                        *)
63
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
64
(*                        énergies alternatives).                         *)
65
(*                                                                        *)
66
(**************************************************************************)
67

    
68
(* this is a prelude for Alt-Ergo*)
69
logic safe_comp_div: int, int -> int
70
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
71
logic safe_comp_mod: int, int -> int
72
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
73
(** The theory BuiltIn_ must be appended to this file*)
74
(** The theory Bool_ must be appended to this file*)
75
(** The theory int_Int_ must be appended to this file*)
76
(** The theory int_Abs_ must be appended to this file*)
77
axiom Div_bound :
78
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
79
  (0 <= safe_comp_div(x,y))))
80

    
81
axiom Div_bound1 :
82
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
83
  (safe_comp_div(x,y) <= x)))
84

    
85
axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))
86

    
87
axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))
88

    
89
axiom Div_inf :
90
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
91
  (safe_comp_div(x,y) = 0)))
92

    
93
axiom Mod_inf :
94
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
95
  (safe_comp_mod(x,y) = x)))
96

    
97
axiom Div_mult :
98
  (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
99
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
100
  (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))
101

    
102
axiom Mod_mult :
103
  (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
104
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
105
  (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))
106

    
107
(**************************************************************************)
108
(*                                                                        *)
109
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
110
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
111
(*                                                                        *)
112
(*  This software is distributed under the terms of the GNU Lesser        *)
113
(*  General Public License version 2.1, with the special exception        *)
114
(*  on linking described in file LICENSE.                                 *)
115
(*                                                                        *)
116
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
117
(*                        énergies alternatives).                         *)
118
(*                                                                        *)
119
(**************************************************************************)
120

    
121
(* this is a prelude for Alt-Ergo*)
122
(* this is a prelude for Alt-Ergo real arithmetic *)
123
(** The theory BuiltIn_ must be appended to this file*)
124
(** The theory Bool_ must be appended to this file*)
125
axiom add_div :
126
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
127
  (((x + y) / z) = ((x / z) + (y / z)))))
128

    
129
axiom sub_div :
130
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
131
  (((x - y) / z) = ((x / z) - (y / z)))))
132

    
133
axiom neg_div :
134
  (forall x:real. forall y:real. ((not (y = 0.0)) ->
135
  (((-x) / y) = (-(x / y)))))
136

    
137
axiom assoc_mul_div :
138
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
139
  (((x * y) / z) = (x * (y / z)))))
140

    
141
axiom assoc_div_mul :
142
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
143
  (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))
144

    
145
axiom assoc_div_div :
146
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
147
  (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))
148

    
149
(**************************************************************************)
150
(*                                                                        *)
151
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
152
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
153
(*                                                                        *)
154
(*  This software is distributed under the terms of the GNU Lesser        *)
155
(*  General Public License version 2.1, with the special exception        *)
156
(*  on linking described in file LICENSE.                                 *)
157
(*                                                                        *)
158
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
159
(*                        énergies alternatives).                         *)
160
(*                                                                        *)
161
(**************************************************************************)
162

    
163
(* this is a prelude for Alt-Ergo*)
164
(** The theory BuiltIn_ must be appended to this file*)
165
(** The theory Bool_ must be appended to this file*)
166
(** The theory real_Real_ must be appended to this file*)
167
(**************************************************************************)
168
(*                                                                        *)
169
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
170
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
171
(*                                                                        *)
172
(*  This software is distributed under the terms of the GNU Lesser        *)
173
(*  General Public License version 2.1, with the special exception        *)
174
(*  on linking described in file LICENSE.                                 *)
175
(*                                                                        *)
176
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
177
(*                        énergies alternatives).                         *)
178
(*                                                                        *)
179
(**************************************************************************)
180

    
181
(* this is a prelude for Alt-Ergo*)
182
(** The theory BuiltIn_ must be appended to this file*)
183
(** The theory Bool_ must be appended to this file*)
184
(** The theory int_Int_ must be appended to this file*)
185
(** The theory real_Real_ must be appended to this file*)
186
logic from_int : int -> real
187

    
188
axiom Zero : (from_int(0) = 0.0)
189

    
190
axiom One : (from_int(1) = 1.0)
191

    
192
axiom Add :
193
  (forall x:int. forall y:int.
194
  (from_int((x + y)) = (from_int(x) + from_int(y))))
195

    
196
axiom Sub :
197
  (forall x:int. forall y:int.
198
  (from_int((x - y)) = (from_int(x) - from_int(y))))
199

    
200
axiom Mul :
201
  (forall x:int. forall y:int.
202
  (from_int((x * y)) = (from_int(x) * from_int(y))))
203

    
204
axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))
205

    
206
(**************************************************************************)
207
(*                                                                        *)
208
(*  This file is part of WP plug-in of Frama-C.                           *)
209
(*                                                                        *)
210
(*  Copyright (C) 2007-2014                                               *)
211
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
212
(*         alternatives)                                                  *)
213
(*                                                                        *)
214
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
215
(*  Lesser General Public License as published by the Free Software       *)
216
(*  Foundation, version 2.1.                                              *)
217
(*                                                                        *)
218
(*  It is distributed in the hope that it will be useful,                 *)
219
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
220
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
221
(*  GNU Lesser General Public License for more details.                   *)
222
(*                                                                        *)
223
(*  See the GNU Lesser General Public License version 2.1                 *)
224
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
225
(*                                                                        *)
226
(**************************************************************************)
227

    
228
(* this is a prelude for Alt-Ergo*)
229
(** The theory BuiltIn_ must be appended to this file*)
230
(** The theory Bool_ must be appended to this file*)
231
(** The theory bool_Bool_ must be appended to this file*)
232
(** The theory int_Int_ must be appended to this file*)
233
(** The theory int_Abs_ must be appended to this file*)
234
(** The theory int_ComputerDivision_ must be appended to this file*)
235
(** The theory real_Real_ must be appended to this file*)
236
(** The theory real_RealInfix_ must be appended to this file*)
237
(** The theory real_FromInt_ must be appended to this file*)
238
logic ite : bool, 'a, 'a -> 'a
239

    
240
axiom ite1 :
241
  (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
242
  (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))
243

    
244
logic eqb : 'a, 'a -> bool
245

    
246
axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))
247

    
248
axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))
249

    
250
logic neqb : 'a, 'a -> bool
251

    
252
axiom neqb1 :
253
  (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))
254

    
255
axiom neqb2 :
256
  (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))
257

    
258
logic zlt : int, int -> bool
259

    
260
logic zleq : int, int -> bool
261

    
262
axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x <  y)))
263

    
264
axiom zlt2 : (forall x:int. forall y:int. ((x <  y) -> (zlt(x, y) = true)))
265

    
266
axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))
267

    
268
axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))
269

    
270
logic rlt : real, real -> bool
271

    
272
logic rleq : real, real -> bool
273

    
274
axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x <  y)))
275

    
276
axiom rlt2 : (forall x:real. forall y:real. ((x <  y) -> (rlt(x, y) = true)))
277

    
278
axiom rleq1 :
279
  (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))
280

    
281
axiom rleq2 :
282
  (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))
283

    
284
logic truncate : real -> int
285

    
286
function real_of_int(x: int) : real = from_int(x)
287

    
288
axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))
289

    
290
axiom c_euclidian :
291
  (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
292
  ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))
293

    
294
axiom cdiv_cases :
295
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 <  d) ->
296
  (safe_comp_div(n,d) = (n / d)))))
297

    
298
axiom cdiv_cases1 :
299
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 <  d) ->
300
  (safe_comp_div(n,d) = (-((-n) / d))))))
301

    
302
axiom cdiv_cases2 :
303
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d <  0) ->
304
  (safe_comp_div(n,d) = (-(n / (-d)))))))
305

    
306
axiom cdiv_cases3 :
307
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d <  0) ->
308
  (safe_comp_div(n,d) = ((-n) / (-d))))))
309

    
310
axiom cmod_cases :
311
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
312
  (safe_comp_mod(n,d) = (n % d)))))
313

    
314
axiom cmod_cases1 :
315
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
316
  (safe_comp_mod(n,d) = (-((-n) % d))))))
317

    
318
axiom cmod_cases2 :
319
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
320
  (safe_comp_mod(n,d) = (n % (-d))))))
321

    
322
axiom cmod_cases3 :
323
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
324
  (safe_comp_mod(n,d) = (-((-n) % (-d)))))))
325

    
326
axiom cmod_remainder :
327
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
328
  (0 <= safe_comp_mod(n,d)))))
329

    
330
axiom cmod_remainder1 :
331
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
332
  (safe_comp_mod(n,d) <  d))))
333

    
334
axiom cmod_remainder2 :
335
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
336
  ((-d) <  safe_comp_mod(n,d)))))
337

    
338
axiom cmod_remainder3 :
339
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
340
  (safe_comp_mod(n,d) <= 0))))
341

    
342
axiom cmod_remainder4 :
343
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
344
  (0 <= safe_comp_mod(n,d)))))
345

    
346
axiom cmod_remainder5 :
347
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
348
  (safe_comp_mod(n,d) <  (-d)))))
349

    
350
axiom cmod_remainder6 :
351
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
352
  (d <  safe_comp_mod(n,d)))))
353

    
354
axiom cmod_remainder7 :
355
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
356
  (safe_comp_mod(n,d) <= 0))))
357

    
358
axiom cdiv_neutral :
359
  (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))
360

    
361
axiom cdiv_inv :
362
  (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
363
  (safe_comp_div(a,a) = 1)))
364

    
365
(**************************************************************************)
366
(*                                                                        *)
367
(*  This file is part of WP plug-in of Frama-C.                           *)
368
(*                                                                        *)
369
(*  Copyright (C) 2007-2014                                               *)
370
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
371
(*         alternatives)                                                  *)
372
(*                                                                        *)
373
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
374
(*  Lesser General Public License as published by the Free Software       *)
375
(*  Foundation, version 2.1.                                              *)
376
(*                                                                        *)
377
(*  It is distributed in the hope that it will be useful,                 *)
378
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
379
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
380
(*  GNU Lesser General Public License for more details.                   *)
381
(*                                                                        *)
382
(*  See the GNU Lesser General Public License version 2.1                 *)
383
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
384
(*                                                                        *)
385
(**************************************************************************)
386

    
387
(* this is a prelude for Alt-Ergo*)
388
(** The theory BuiltIn_ must be appended to this file*)
389
(** The theory Bool_ must be appended to this file*)
390
(** The theory bool_Bool_ must be appended to this file*)
391
(** The theory int_Int_ must be appended to this file*)
392
logic is_uint8 : int -> prop
393

    
394
axiom is_uint8_def : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (0 <= x)))
395

    
396
axiom is_uint8_def1 :
397
  (forall x:int [is_uint8(x)]. (is_uint8(x) -> (x <  256)))
398

    
399
axiom is_uint8_def2 :
400
  (forall x:int [is_uint8(x)]. (((0 <= x) and (x <  256)) -> is_uint8(x)))
401

    
402
logic is_sint8 : int -> prop
403

    
404
axiom is_sint8_def :
405
  (forall x:int [is_sint8(x)]. (is_sint8(x) -> ((-128) <= x)))
406

    
407
axiom is_sint8_def1 :
408
  (forall x:int [is_sint8(x)]. (is_sint8(x) -> (x <  128)))
409

    
410
axiom is_sint8_def2 :
411
  (forall x:int [is_sint8(x)]. ((((-128) <= x) and (x <  128)) ->
412
  is_sint8(x)))
413

    
414
logic is_uint16 : int -> prop
415

    
416
axiom is_uint16_def :
417
  (forall x:int [is_uint16(x)]. (is_uint16(x) -> (0 <= x)))
418

    
419
axiom is_uint16_def1 :
420
  (forall x:int [is_uint16(x)]. (is_uint16(x) -> (x <  65536)))
421

    
422
axiom is_uint16_def2 :
423
  (forall x:int [is_uint16(x)]. (((0 <= x) and (x <  65536)) ->
424
  is_uint16(x)))
425

    
426
predicate is_sint16(x: int) = (((-32768) <= x) and (x <  32768))
427

    
428
logic is_uint32 : int -> prop
429

    
430
axiom is_uint32_def :
431
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x)))
432

    
433
axiom is_uint32_def1 :
434
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (x <  4294967296)))
435

    
436
axiom is_uint32_def2 :
437
  (forall x:int [is_uint32(x)]. (((0 <= x) and (x <  4294967296)) ->
438
  is_uint32(x)))
439

    
440
logic is_sint32 : int -> prop
441

    
442
axiom is_sint32_def :
443
  (forall x:int [is_sint32(x)]. (is_sint32(x) -> ((-2147483648) <= x)))
444

    
445
axiom is_sint32_def1 :
446
  (forall x:int [is_sint32(x)]. (is_sint32(x) -> (x <  2147483648)))
447

    
448
axiom is_sint32_def2 :
449
  (forall x:int [is_sint32(x)]. ((((-2147483648) <= x) and
450
  (x <  2147483648)) -> is_sint32(x)))
451

    
452
logic is_uint64 : int -> prop
453

    
454
axiom is_uint64_def :
455
  (forall x:int [is_uint64(x)]. (is_uint64(x) -> (0 <= x)))
456

    
457
axiom is_uint64_def1 :
458
  (forall x:int [is_uint64(x)]. (is_uint64(x) ->
459
  (x <  18446744073709551616)))
460

    
461
axiom is_uint64_def2 :
462
  (forall x:int [is_uint64(x)]. (((0 <= x) and
463
  (x <  18446744073709551616)) -> is_uint64(x)))
464

    
465
logic is_sint64 : int -> prop
466

    
467
axiom is_sint64_def :
468
  (forall x:int [is_sint64(x)]. (is_sint64(x) ->
469
  ((-9223372036854775808) <= x)))
470

    
471
axiom is_sint64_def1 :
472
  (forall x:int [is_sint64(x)]. (is_sint64(x) -> (x <  9223372036854775808)))
473

    
474
axiom is_sint64_def2 :
475
  (forall x:int [is_sint64(x)]. ((((-9223372036854775808) <= x) and
476
  (x <  9223372036854775808)) -> is_sint64(x)))
477

    
478
logic to_uint8 : int -> int
479

    
480
logic to_sint8 : int -> int
481

    
482
logic to_uint16 : int -> int
483

    
484
logic to_sint16 : int -> int
485

    
486
logic to_uint32 : int -> int
487

    
488
logic to_sint32 : int -> int
489

    
490
logic to_uint64 : int -> int
491

    
492
logic to_sint64 : int -> int
493

    
494
axiom is_to_uint8 :
495
  (forall x:int [is_uint8(to_uint8(x))]. is_uint8(to_uint8(x)))
496

    
497
axiom is_to_sint8 :
498
  (forall x:int [is_sint8(to_sint8(x))]. is_sint8(to_sint8(x)))
499

    
500
axiom is_to_uint16 :
501
  (forall x:int [is_uint16(to_uint16(x))]. is_uint16(to_uint16(x)))
502

    
503
axiom is_to_sint16 :
504
  (forall x:int [is_sint16(to_sint16(x))]. is_sint16(to_sint16(x)))
505

    
506
axiom is_to_uint32 :
507
  (forall x:int [is_uint32(to_uint32(x))]. is_uint32(to_uint32(x)))
508

    
509
axiom is_to_sint32 :
510
  (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
511

    
512
axiom is_to_uint64 :
513
  (forall x:int [is_uint64(to_uint64(x))]. is_uint64(to_uint64(x)))
514

    
515
axiom is_to_sint64 :
516
  (forall x:int [is_sint64(to_sint64(x))]. is_sint64(to_sint64(x)))
517

    
518
axiom id_uint8 :
519
  (forall x:int [to_uint8(x)]. (((0 <= x) and (x <  256)) ->
520
  (to_uint8(x) = x)))
521

    
522
axiom id_sint8 :
523
  (forall x:int [to_sint8(x)]. ((((-128) <= x) and (x <  128)) ->
524
  (to_sint8(x) = x)))
525

    
526
axiom id_uint16 :
527
  (forall x:int [to_uint16(x)]. (((0 <= x) and (x <  65536)) ->
528
  (to_uint16(x) = x)))
529

    
530
axiom id_sint16 :
531
  (forall x:int [to_sint16(x)]. ((((-32768) <= x) and (x <  32768)) ->
532
  (to_sint16(x) = x)))
533

    
534
axiom id_uint32 :
535
  (forall x:int [to_uint32(x)]. (((0 <= x) and (x <  4294967296)) ->
536
  (to_uint32(x) = x)))
537

    
538
axiom id_sint32 :
539
  (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
540
  (x <  2147483648)) -> (to_sint32(x) = x)))
541

    
542
axiom id_uint64 :
543
  (forall x:int [to_uint64(x)]. (((0 <= x) and
544
  (x <  18446744073709551616)) -> (to_uint64(x) = x)))
545

    
546
axiom id_sint64 :
547
  (forall x:int [to_sint64(x)]. ((((-9223372036854775808) <= x) and
548
  (x <  9223372036854775808)) -> (to_sint64(x) = x)))
549

    
550
logic lnot : int -> int
551

    
552
logic ac land : int, int -> int
553

    
554
logic ac lxor : int, int -> int
555

    
556
logic ac lor : int, int -> int
557

    
558
logic lsl : int, int -> int
559

    
560
logic lsr : int, int -> int
561

    
562
logic bit_testb : int, int -> bool
563

    
564
logic bit_test : int, int -> prop
565

    
566
(* ---------------------------------------------------------- *)
567
(* --- Global Definitions                                 --- *)
568
(* ---------------------------------------------------------- *)
569

    
570
predicate P_trans_totoA() = true
571

    
572
predicate P_clock_d() = true
573

    
574
predicate P_trans_d
575
    (x:int,
576
    d:int) =
577
    ((0 = d) and (x <= 0)) or ((1 = d) and (0 < x))
578

    
579
predicate P_trans_totoB
580
    (x:int,
581
    d:int) =
582
    P_trans_totoA and (P_clock_d -> P_trans_d(x, d))
583

    
584
predicate P_clock_toto_2(d:int) = 1 = d
585

    
586
predicate P_trans_toto_2(x:int, toto_2_0:int) = (0 = x) <-> (0 <> toto_2_0)
587

    
588
predicate P_trans_totoC
589
    (x:int,
590
    d:int,
591
    toto_2_0:int) =
592
    P_trans_totoB(x, d) and
593
    (P_clock_toto_2(d) -> P_trans_toto_2(x, toto_2_0))
594

    
595
predicate P_clock_c(d:int) = 1 = d
596

    
597
predicate P_trans_c
598
    (toto_2_0:int,
599
    c:int) =
600
    ((0 = c) and (0 <> toto_2_0)) or ((0 = toto_2_0) and (1 = c))
601

    
602
predicate P_trans_totoD
603
    (x:int,
604
    d:int,
605
    c:int) =
606
    exists i : int. is_uint32(i) and P_trans_totoC(x, d, i) and
607
    (P_clock_c(d) -> P_trans_c(i, c))
608

    
609
predicate P_clock_b2(d:int, c:int) = (0 = c) and P_clock_c(d)
610

    
611
predicate P_trans_b2(b2_0:int) = 2 = b2_0
612

    
613
predicate P_trans_totoE
614
    (x:int,
615
    d:int,
616
    c:int,
617
    b2_0:int) =
618
    P_trans_totoD(x, d, c) and (P_clock_b2(d, c) -> P_trans_b2(b2_0))
619

    
620
predicate P_clock_b1(d:int, c:int) = (1 = c) and P_clock_c(d)
621

    
622
predicate P_trans_b1(b1_0:int) = 1 = b1_0
623

    
624
predicate P_trans_totoF
625
    (x:int,
626
    d:int,
627
    c:int,
628
    b2_0:int,
629
    b1_0:int) =
630
    P_trans_totoE(x, d, c, b2_0) and (P_clock_b1(d, c) -> P_trans_b1(b1_0))
631

    
632
predicate P_clock_z(d:int) = P_clock_c(d)
633

    
634
predicate P_trans_z
635
    (c:int,
636
    b1_0:int,
637
    b2_0:int,
638
    z:int) =
639
    ((1 = c) -> (b1_0 = z)) and ((0 = c) -> (b2_0 = z))
640

    
641
predicate P_trans_totoG
642
    (x:int,
643
    d:int,
644
    z:int) =
645
    exists i_2,i_1,i : int. is_sint32(i) and is_sint32(i_1) and
646
    is_uint32(i_2) and P_trans_totoF(x, d, i_2, i_1, i) and
647
    (P_clock_z(d) -> P_trans_z(i_2, i, i_1, z))
648

    
649
predicate P_clock_b3(d:int) = 0 = d
650

    
651
predicate P_trans_b3(b3_0:int) = 3 = b3_0
652

    
653
predicate P_trans_totoH
654
    (x:int,
655
    d:int,
656
    z:int,
657
    b3_0:int) =
658
    P_trans_totoG(x, d, z) and (P_clock_b3(d) -> P_trans_b3(b3_0))
659

    
660
predicate P_clock_y() = P_clock_d
661

    
662
predicate P_trans_y
663
    (d:int,
664
    b3_0:int,
665
    z:int,
666
    y:int) =
667
    ((0 = d) -> (b3_0 = y)) and ((1 = d) -> (y = z))
668

    
669
predicate P_trans_totoI
670
    (x:int,
671
    y:int) =
672
    exists i_2,i_1,i : int. is_sint32(i_1) and is_sint32(i_2) and
673
    is_uint32(i) and P_trans_totoH(x, i, i_2, i_1) and
674
    (P_clock_y -> P_trans_y(i, i_1, i_2, y))
675

    
676
(**************************************************************************)
677
(*                                                                        *)
678
(*  This file is part of WP plug-in of Frama-C.                           *)
679
(*                                                                        *)
680
(*  Copyright (C) 2007-2014                                               *)
681
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
682
(*         alternatives)                                                  *)
683
(*                                                                        *)
684
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
685
(*  Lesser General Public License as published by the Free Software       *)
686
(*  Foundation, version 2.1.                                              *)
687
(*                                                                        *)
688
(*  It is distributed in the hope that it will be useful,                 *)
689
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
690
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
691
(*  GNU Lesser General Public License for more details.                   *)
692
(*                                                                        *)
693
(*  See the GNU Lesser General Public License version 2.1                 *)
694
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
695
(*                                                                        *)
696
(**************************************************************************)
697

    
698
(* this is a prelude for Alt-Ergo*)
699
(** The theory BuiltIn_ must be appended to this file*)
700
(** The theory Bool_ must be appended to this file*)
701
(** The theory bool_Bool_ must be appended to this file*)
702
(** The theory int_Int_ must be appended to this file*)
703
(** The theory map_Map_ must be appended to this file*)
704
type addr = { base : int; offset : int
705
}
706

    
707
logic addr_le : addr, addr -> prop
708

    
709
logic addr_lt : addr, addr -> prop
710

    
711
logic addr_le_bool : addr, addr -> bool
712

    
713
logic addr_lt_bool : addr, addr -> bool
714

    
715
axiom addr_le_def :
716
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
717
  (addr_le(p, q) -> ((p).offset <= (q).offset))))
718

    
719
axiom addr_le_def1 :
720
  (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
721
  (((p).offset <= (q).offset) -> addr_le(p, q))))
722

    
723
axiom addr_lt_def :
724
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
725
  (addr_lt(p, q) -> ((p).offset <  (q).offset))))
726

    
727
axiom addr_lt_def1 :
728
  (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
729
  (((p).offset <  (q).offset) -> addr_lt(p, q))))
730

    
731
axiom addr_le_bool_def :
732
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) ->
733
  (addr_le_bool(p, q) = true)))
734

    
735
axiom addr_le_bool_def1 :
736
  (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p,
737
  q) = true) -> addr_le(p, q)))
738

    
739
axiom addr_lt_bool_def :
740
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) ->
741
  (addr_lt_bool(p, q) = true)))
742

    
743
axiom addr_lt_bool_def1 :
744
  (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p,
745
  q) = true) -> addr_lt(p, q)))
746

    
747
function null() : addr = { base = 0; offset = 0 }
748

    
749
function global(b: int) : addr = { base = b; offset = 0 }
750

    
751
function shift(p: addr, k: int) : addr = { base = (p).base; offset =
752
  ((p).offset + k) }
753

    
754
predicate included(p: addr, a: int, q: addr, b: int) = ((0 <  a) ->
755
  ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and
756
  (((p).offset + a) <= ((q).offset + b))))))
757

    
758
predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or
759
  ((b <= 0) or ((not ((p).base = (q).base)) or
760
  ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset)))))
761

    
762
predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
763
  a1: int) =
764
  (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) ->
765
  ((m1[q]) = (m2[q]))))
766

    
767
predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
768
  a1: int) =
769
  (forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) ->
770
  ((m1[q]) = (m2[q]))))
771

    
772
predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
773
  ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))
774

    
775
predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
776
  ((0 <  (p).base) and ((0 <= (p).offset) and
777
  (((p).offset + n) <= (m[(p).base])))))
778

    
779
axiom valid_rw_rd :
780
  (forall m:(int,int) farray.
781
  (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n)))))
782

    
783
axiom valid_string :
784
  (forall m:(int,int) farray.
785
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
786
  ((p).offset <  (m[(p).base]))) -> valid_rd(m, p, 1)))))
787

    
788
axiom valid_string1 :
789
  (forall m:(int,int) farray.
790
  (forall p:addr. (((p).base <  0) -> (((0 <= (p).offset) and
791
  ((p).offset <  (m[(p).base]))) -> (not valid_rw(m, p, 1))))))
792

    
793
axiom separated_1 :
794
  (forall p:addr. forall q:addr.
795
  (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q,
796
  b), { base = (p).base; offset = i }, { base = (q).base; offset = j }].
797
  (separated(p, a, q, b) -> ((((p).offset <= i) and
798
  (i <  ((p).offset + a))) -> ((((q).offset <= j) and
799
  (j <  ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = {
800
  base = (q).base; offset = j })))))))
801

    
802
logic region : int -> int
803

    
804
logic linked : (int,int) farray -> prop
805

    
806
logic sconst : (addr,int) farray -> prop
807

    
808
predicate framed(m: (addr,addr) farray) =
809
  (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0))
810

    
811
axiom separated_included :
812
  (forall p:addr. forall q:addr.
813
  (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)].
814
  ((0 <  a) -> ((0 <  b) -> (separated(p, a, q, b) -> (not included(p, a, q,
815
  b)))))))
816

    
817
axiom included_trans :
818
  (forall p:addr. forall q:addr. forall r:addr.
819
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
820
  included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) ->
821
  included(p, a, r, c)))))
822

    
823
axiom separated_trans :
824
  (forall p:addr. forall q:addr. forall r:addr.
825
  (forall a:int. forall b:int. forall c:int [included(p, a, q, b),
826
  separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) ->
827
  separated(p, a, r, c)))))
828

    
829
axiom separated_sym :
830
  (forall p:addr. forall q:addr.
831
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q,
832
  b) -> separated(q, b, p, a))))
833

    
834
axiom separated_sym1 :
835
  (forall p:addr. forall q:addr.
836
  (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p,
837
  a) -> separated(p, a, q, b))))
838

    
839
axiom eqmem_included :
840
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
841
  (forall p:addr. forall q:addr.
842
  (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)].
843
  (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1))))))
844

    
845
axiom eqmem_sym :
846
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
847
  (forall p:addr.
848
  (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1)))))
849

    
850
axiom havoc_sym :
851
  (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
852
  (forall p:addr.
853
  (forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1)))))
854

    
855
logic cast : addr -> int
856

    
857
axiom cast_injective :
858
  (forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) ->
859
  (p = q)))
860

    
861
logic hardware : int -> int
862

    
863
axiom hardnull : (hardware(0) = 0)
864

    
865
(* ---------------------------------------------------------- *)
866
(* --- Assertion (file clocks7/clocks7_7.c, line 184)     --- *)
867
(* ---------------------------------------------------------- *)
868

    
869
goal toto_step_assert_20:
870
  forall i : int.
871
  forall t_3,t_2,t_1,t : (addr,int) farray.
872
  forall a : addr.
873
  P_trans_totoA ->
874
  (i <= 0) ->
875
  P_clock_b3(0) ->
876
  is_sint32(i) ->
877
  is_sint32(t[a]) ->
878
  is_sint32(t_1[a]) ->
879
  is_sint32(t_2[a]) ->
880
  is_sint32(t_3[a]) ->
881
  P_trans_totoB(i, 0) ->
882
  (region(a.base) <= 0) ->
883
  (P_clock_d -> P_trans_d(i, 0)) ->
884
  P_trans_b3(3)
885