notinc_disj_FT.ft_is_a_pred_why.why 85.9 KB
Newer Older
François Bobot's avatar
François Bobot committed
1
theory Why2
2
use array.Array as A
3
  use unit_inf.Unit
François Bobot's avatar
François Bobot committed
4 5 6
  use int.Int
  use int.ComputerDivision
  use real.Real
7
  use bool_inf.Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
8
  predicate eq_unit Unit.unit Unit.unit
François Bobot's avatar
François Bobot committed
9

Andrei Paskevich's avatar
Andrei Paskevich committed
10
  predicate neq_unit Unit.unit Unit.unit
François Bobot's avatar
François Bobot committed
11

Andrei Paskevich's avatar
Andrei Paskevich committed
12
  predicate eq_bool Bool.bool Bool.bool
François Bobot's avatar
François Bobot committed
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
  predicate neq_bool Bool.bool Bool.bool
François Bobot's avatar
François Bobot committed
15

Andrei Paskevich's avatar
Andrei Paskevich committed
16
  predicate lt_int int int
François Bobot's avatar
François Bobot committed
17

Andrei Paskevich's avatar
Andrei Paskevich committed
18
  predicate le_int int int
François Bobot's avatar
François Bobot committed
19

Andrei Paskevich's avatar
Andrei Paskevich committed
20
  predicate gt_int int int
François Bobot's avatar
François Bobot committed
21

Andrei Paskevich's avatar
Andrei Paskevich committed
22
  predicate ge_int int int
François Bobot's avatar
François Bobot committed
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24
  predicate eq_int int int
François Bobot's avatar
François Bobot committed
25

Andrei Paskevich's avatar
Andrei Paskevich committed
26
  predicate neq_int int int
François Bobot's avatar
François Bobot committed
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28
  function add_int int int : int
François Bobot's avatar
François Bobot committed
29

Andrei Paskevich's avatar
Andrei Paskevich committed
30
  function sub_int int int : int
François Bobot's avatar
François Bobot committed
31

Andrei Paskevich's avatar
Andrei Paskevich committed
32
  function mul_int int int : int
François Bobot's avatar
François Bobot committed
33

Andrei Paskevich's avatar
Andrei Paskevich committed
34
  function div_int int int : int
François Bobot's avatar
François Bobot committed
35

Andrei Paskevich's avatar
Andrei Paskevich committed
36
  function mod_int int int : int
François Bobot's avatar
François Bobot committed
37

Andrei Paskevich's avatar
Andrei Paskevich committed
38
  function neg_int int : int
François Bobot's avatar
François Bobot committed
39

Andrei Paskevich's avatar
Andrei Paskevich committed
40
  predicate zwf_zero int int
François Bobot's avatar
François Bobot committed
41 42 43 44

  axiom Zwf_zero_def:
    (forall a0:int.
      (forall b0:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
45 46
        (((Int.(<=) 0 b0) /\ (Int.(<) a0 b0)) <->
         ((Int.(<=) 0 b0) /\ (Int.(<) a0 b0)))))
François Bobot's avatar
François Bobot committed
47

Andrei Paskevich's avatar
Andrei Paskevich committed
48
  function bool_and Bool.bool Bool.bool : Bool.bool
François Bobot's avatar
François Bobot committed
49

Andrei Paskevich's avatar
Andrei Paskevich committed
50
  function bool_or Bool.bool Bool.bool : Bool.bool
François Bobot's avatar
François Bobot committed
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52
  function bool_xor Bool.bool Bool.bool : Bool.bool
François Bobot's avatar
François Bobot committed
53

Andrei Paskevich's avatar
Andrei Paskevich committed
54
  function bool_not Bool.bool : Bool.bool
François Bobot's avatar
François Bobot committed
55 56 57 58

  axiom Bool_and_def:
    (forall a:Bool.bool.
      (forall b:Bool.bool.
59
        (((bool_and a b : Bool.bool) = Bool.ttrue) <->
Andrei Paskevich's avatar
Andrei Paskevich committed
60
         ((a = Bool.ttrue) /\ (b = Bool.ttrue)))))
François Bobot's avatar
François Bobot committed
61 62 63 64

  axiom Bool_or_def:
    (forall a:Bool.bool.
      (forall b:Bool.bool.
65
        (((bool_or a b : Bool.bool) = Bool.ttrue) <->
Andrei Paskevich's avatar
Andrei Paskevich committed
66
         ((a = Bool.ttrue) \/ (b = Bool.ttrue)))))
François Bobot's avatar
François Bobot committed
67 68 69 70

  axiom Bool_xor_def:
    (forall a:Bool.bool.
      (forall b:Bool.bool.
71
        (((bool_xor a b : Bool.bool) = Bool.ttrue) <-> (a <> b))))
François Bobot's avatar
François Bobot committed
72 73 74

  axiom Bool_not_def:
    (forall a:Bool.bool.
75
      (((bool_not a : Bool.bool) = Bool.ttrue) <-> (a = Bool.ffalse)))
François Bobot's avatar
François Bobot committed
76

Andrei Paskevich's avatar
Andrei Paskevich committed
77
  function ite Bool.bool 'a1 'a1 : 'a1
François Bobot's avatar
François Bobot committed
78 79

  axiom Ite_true:
80
    (forall x:'a1. (forall y:'a1. ((ite Bool.ttrue x y : 'a1) = x)))
François Bobot's avatar
François Bobot committed
81 82

  axiom Ite_false:
83
    (forall x:'a1. (forall y:'a1. ((ite Bool.ffalse x y : 'a1) = y)))
François Bobot's avatar
François Bobot committed
84

Andrei Paskevich's avatar
Andrei Paskevich committed
85
  function lt_int_bool int int : Bool.bool
François Bobot's avatar
François Bobot committed
86

Andrei Paskevich's avatar
Andrei Paskevich committed
87
  function le_int_bool int int : Bool.bool
François Bobot's avatar
François Bobot committed
88

Andrei Paskevich's avatar
Andrei Paskevich committed
89
  function gt_int_bool int int : Bool.bool
François Bobot's avatar
François Bobot committed
90

Andrei Paskevich's avatar
Andrei Paskevich committed
91
  function ge_int_bool int int : Bool.bool
François Bobot's avatar
François Bobot committed
92

Andrei Paskevich's avatar
Andrei Paskevich committed
93
  function eq_int_bool int int : Bool.bool
François Bobot's avatar
François Bobot committed
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95
  function neq_int_bool int int : Bool.bool
François Bobot's avatar
François Bobot committed
96 97 98 99

  axiom Lt_int_bool_axiom:
    (forall x:int.
      (forall y:int.
100
        (((lt_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(<) x y))))
François Bobot's avatar
François Bobot committed
101 102 103 104

  axiom Le_int_bool_axiom:
    (forall x:int.
      (forall y:int.
105
        (((le_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(<=) x y))))
François Bobot's avatar
François Bobot committed
106 107 108 109

  axiom Gt_int_bool_axiom:
    (forall x:int.
      (forall y:int.
110
        (((gt_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(>) x y))))
François Bobot's avatar
François Bobot committed
111 112 113 114

  axiom Ge_int_bool_axiom:
    (forall x:int.
      (forall y:int.
115
        (((ge_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(>=) x y))))
François Bobot's avatar
François Bobot committed
116 117 118 119

  axiom Eq_int_bool_axiom:
    (forall x:int.
      (forall y:int.
120
        (((eq_int_bool x y : Bool.bool) = Bool.ttrue) <-> (x = y))))
François Bobot's avatar
François Bobot committed
121 122 123 124

  axiom Neq_int_bool_axiom:
    (forall x:int.
      (forall y:int.
125
        (((neq_int_bool x y : Bool.bool) = Bool.ttrue) <-> (x <> y))))
François Bobot's avatar
François Bobot committed
126

Andrei Paskevich's avatar
Andrei Paskevich committed
127
  function abs_int int : int
François Bobot's avatar
François Bobot committed
128 129 130 131 132 133 134 135

  axiom Abs_int_pos:
    (forall x:int. ((Int.(>=) x 0) -> ((abs_int x : int) = x)))

  axiom Abs_int_neg:
    (forall x:int.
      ((Int.(<=) x 0) -> ((abs_int x : int) = (Int.(-_) x : int))))

Andrei Paskevich's avatar
Andrei Paskevich committed
136
  function int_max int int : int
François Bobot's avatar
François Bobot committed
137

Andrei Paskevich's avatar
Andrei Paskevich committed
138
  function int_min int int : int
François Bobot's avatar
François Bobot committed
139 140 141 142

  axiom Int_max_is_ge:
    (forall x:int.
      (forall y:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
143
        ((Int.(>=) (int_max x y : int) x) /\
François Bobot's avatar
François Bobot committed
144 145 146 147 148
         (Int.(>=) (int_max x y : int) y))))

  axiom Int_max_is_some:
    (forall x:int.
      (forall y:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
149
        (((int_max x y : int) = x) \/ ((int_max x y : int) = y))))
François Bobot's avatar
François Bobot committed
150 151 152 153

  axiom Int_min_is_le:
    (forall x:int.
      (forall y:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
154
        ((Int.(<=) (int_min x y : int) x) /\
François Bobot's avatar
François Bobot committed
155 156 157 158 159
         (Int.(<=) (int_min x y : int) y))))

  axiom Int_min_is_some:
    (forall x:int.
      (forall y:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
160
        (((int_min x y : int) = x) \/ ((int_min x y : int) = y))))
François Bobot's avatar
François Bobot committed
161

Andrei Paskevich's avatar
Andrei Paskevich committed
162
  predicate lt_real real real
François Bobot's avatar
François Bobot committed
163

Andrei Paskevich's avatar
Andrei Paskevich committed
164
  predicate le_real real real
François Bobot's avatar
François Bobot committed
165

Andrei Paskevich's avatar
Andrei Paskevich committed
166
  predicate gt_real real real
François Bobot's avatar
François Bobot committed
167

Andrei Paskevich's avatar
Andrei Paskevich committed
168
  predicate ge_real real real
François Bobot's avatar
François Bobot committed
169

Andrei Paskevich's avatar
Andrei Paskevich committed
170
  predicate eq_real real real
François Bobot's avatar
François Bobot committed
171

Andrei Paskevich's avatar
Andrei Paskevich committed
172
  predicate neq_real real real
François Bobot's avatar
François Bobot committed
173

Andrei Paskevich's avatar
Andrei Paskevich committed
174
  function add_real real real : real
François Bobot's avatar
François Bobot committed
175

Andrei Paskevich's avatar
Andrei Paskevich committed
176
  function sub_real real real : real
François Bobot's avatar
François Bobot committed
177

Andrei Paskevich's avatar
Andrei Paskevich committed
178
  function mul_real real real : real
François Bobot's avatar
François Bobot committed
179

Andrei Paskevich's avatar
Andrei Paskevich committed
180
  function div_real real real : real
François Bobot's avatar
François Bobot committed
181

Andrei Paskevich's avatar
Andrei Paskevich committed
182
  function neg_real real : real
François Bobot's avatar
François Bobot committed
183

Andrei Paskevich's avatar
Andrei Paskevich committed
184
  function real_of_int int : real
François Bobot's avatar
François Bobot committed
185

Andrei Paskevich's avatar
Andrei Paskevich committed
186
  function int_of_real real : int
François Bobot's avatar
François Bobot committed
187

Andrei Paskevich's avatar
Andrei Paskevich committed
188
  function lt_real_bool real real : Bool.bool
François Bobot's avatar
François Bobot committed
189

Andrei Paskevich's avatar
Andrei Paskevich committed
190
  function le_real_bool real real : Bool.bool
François Bobot's avatar
François Bobot committed
191

Andrei Paskevich's avatar
Andrei Paskevich committed
192
  function gt_real_bool real real : Bool.bool
François Bobot's avatar
François Bobot committed
193

Andrei Paskevich's avatar
Andrei Paskevich committed
194
  function ge_real_bool real real : Bool.bool
François Bobot's avatar
François Bobot committed
195

Andrei Paskevich's avatar
Andrei Paskevich committed
196
  function eq_real_bool real real : Bool.bool
François Bobot's avatar
François Bobot committed
197

Andrei Paskevich's avatar
Andrei Paskevich committed
198
  function neq_real_bool real real : Bool.bool
François Bobot's avatar
François Bobot committed
199 200 201 202

  axiom Lt_real_bool_axiom:
    (forall x:real.
      (forall y:real.
203
        (((lt_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(<) x y))))
François Bobot's avatar
François Bobot committed
204 205 206 207

  axiom Le_real_bool_axiom:
    (forall x:real.
      (forall y:real.
208
        (((le_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(<=) x y))))
François Bobot's avatar
François Bobot committed
209 210 211 212

  axiom Gt_real_bool_axiom:
    (forall x:real.
      (forall y:real.
213
        (((gt_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(>) x y))))
François Bobot's avatar
François Bobot committed
214 215 216 217

  axiom Ge_real_bool_axiom:
    (forall x:real.
      (forall y:real.
218
        (((ge_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(>=) x y))))
François Bobot's avatar
François Bobot committed
219 220 221 222

  axiom Eq_real_bool_axiom:
    (forall x:real.
      (forall y:real.
223
        (((eq_real_bool x y : Bool.bool) = Bool.ttrue) <-> (x = y))))
François Bobot's avatar
François Bobot committed
224 225 226 227

  axiom Neq_real_bool_axiom:
    (forall x:real.
      (forall y:real.
228
        (((neq_real_bool x y : Bool.bool) = Bool.ttrue) <-> (x <> y))))
François Bobot's avatar
François Bobot committed
229

Andrei Paskevich's avatar
Andrei Paskevich committed
230
  function real_max real real : real
François Bobot's avatar
François Bobot committed
231

Andrei Paskevich's avatar
Andrei Paskevich committed
232
  function real_min real real : real
François Bobot's avatar
François Bobot committed
233 234 235 236

  axiom Real_max_is_ge:
    (forall x:real.
      (forall y:real.
Andrei Paskevich's avatar
Andrei Paskevich committed
237
        ((Real.(>=) (real_max x y : real) x) /\
François Bobot's avatar
François Bobot committed
238 239 240 241 242
         (Real.(>=) (real_max x y : real) y))))

  axiom Real_max_is_some:
    (forall x:real.
      (forall y:real.
Andrei Paskevich's avatar
Andrei Paskevich committed
243
        (((real_max x y : real) = x) \/ ((real_max x y : real) = y))))
François Bobot's avatar
François Bobot committed
244 245 246 247

  axiom Real_min_is_le:
    (forall x:real.
      (forall y:real.
Andrei Paskevich's avatar
Andrei Paskevich committed
248
        ((Real.(<=) (real_min x y : real) x) /\
François Bobot's avatar
François Bobot committed
249 250 251 252 253
         (Real.(<=) (real_min x y : real) y))))

  axiom Real_min_is_some:
    (forall x:real.
      (forall y:real.
Andrei Paskevich's avatar
Andrei Paskevich committed
254
        (((real_min x y : real) = x) \/ ((real_min x y : real) = y))))
François Bobot's avatar
François Bobot committed
255

Andrei Paskevich's avatar
Andrei Paskevich committed
256
  function sqrt_real real : real
François Bobot's avatar
François Bobot committed
257

Andrei Paskevich's avatar
Andrei Paskevich committed
258
  function pow_real real real : real
François Bobot's avatar
François Bobot committed
259

Andrei Paskevich's avatar
Andrei Paskevich committed
260
  function abs_real real : real
François Bobot's avatar
François Bobot committed
261 262 263 264 265 266 267 268 269

  axiom Abs_real_pos:
    (forall x:real [(abs_real x : real)].
      ((Real.(>=) x 0.0) -> ((abs_real x : real) = x)))

  axiom Abs_real_neg:
    (forall x:real [(abs_real x : real)].
      ((Real.(<=) x 0.0) -> ((abs_real x : real) = (Real.(-_) x : real))))

Andrei Paskevich's avatar
Andrei Paskevich committed
270
  function exp real : real
François Bobot's avatar
François Bobot committed
271

Andrei Paskevich's avatar
Andrei Paskevich committed
272
  function log real : real
François Bobot's avatar
François Bobot committed
273

Andrei Paskevich's avatar
Andrei Paskevich committed
274
  function log10 real : real
François Bobot's avatar
François Bobot committed
275 276 277

  axiom Log_exp: (forall x:real. ((log (exp x : real) : real) = x))

Andrei Paskevich's avatar
Andrei Paskevich committed
278
  function cos real : real
François Bobot's avatar
François Bobot committed
279

Andrei Paskevich's avatar
Andrei Paskevich committed
280
  function sin real : real
François Bobot's avatar
François Bobot committed
281

Andrei Paskevich's avatar
Andrei Paskevich committed
282
  function tan real : real
François Bobot's avatar
François Bobot committed
283

Andrei Paskevich's avatar
Andrei Paskevich committed
284
  function cosh real : real
François Bobot's avatar
François Bobot committed
285

Andrei Paskevich's avatar
Andrei Paskevich committed
286
  function sinh real : real
François Bobot's avatar
François Bobot committed
287

Andrei Paskevich's avatar
Andrei Paskevich committed
288
  function tanh real : real
François Bobot's avatar
François Bobot committed
289

Andrei Paskevich's avatar
Andrei Paskevich committed
290
  function acos real : real
François Bobot's avatar
François Bobot committed
291

Andrei Paskevich's avatar
Andrei Paskevich committed
292
  function asin real : real
François Bobot's avatar
François Bobot committed
293

Andrei Paskevich's avatar
Andrei Paskevich committed
294
  function atan real : real
François Bobot's avatar
François Bobot committed
295

Andrei Paskevich's avatar
Andrei Paskevich committed
296
  function atan2 real real : real
François Bobot's avatar
François Bobot committed
297

Andrei Paskevich's avatar
Andrei Paskevich committed
298
  function hypot real real : real
François Bobot's avatar
François Bobot committed
299 300 301 302 303 304 305

  type alloc_table 't

  type pointer 't

  type block 't

Andrei Paskevich's avatar
Andrei Paskevich committed
306
  function base_block (pointer 'a1) : (block 'a1)
François Bobot's avatar
François Bobot committed
307

Andrei Paskevich's avatar
Andrei Paskevich committed
308
  function pointer_address (pointer 'a1) : (pointer Unit.unit)
François Bobot's avatar
François Bobot committed
309

Andrei Paskevich's avatar
Andrei Paskevich committed
310
  function absolute_address int : (pointer Unit.unit)
François Bobot's avatar
François Bobot committed
311

Andrei Paskevich's avatar
Andrei Paskevich committed
312
  function address (pointer 'a1) : int
François Bobot's avatar
François Bobot committed
313

Andrei Paskevich's avatar
Andrei Paskevich committed
314
  function offset_max (alloc_table 'a1) (pointer 'a1) : int
François Bobot's avatar
François Bobot committed
315

Andrei Paskevich's avatar
Andrei Paskevich committed
316
  function offset_min (alloc_table 'a1) (pointer 'a1) : int
François Bobot's avatar
François Bobot committed
317

Andrei Paskevich's avatar
Andrei Paskevich committed
318
  predicate valid (alloc_table 'a1) (pointer 'a1)
François Bobot's avatar
François Bobot committed
319 320 321 322 323

  axiom Valid_def:
    (forall a0:(alloc_table 'a1).
      (forall p0:(pointer 'a1).
        ((valid a0 p0) <->
Andrei Paskevich's avatar
Andrei Paskevich committed
324
         ((Int.(<=) (offset_min a0 p0 : int) 0) /\
François Bobot's avatar
François Bobot committed
325 326
          (Int.(>=) (offset_max a0 p0 : int) 0)))))

Andrei Paskevich's avatar
Andrei Paskevich committed
327
  predicate same_block (pointer 'a1) (pointer 'a1)
François Bobot's avatar
François Bobot committed
328 329 330 331 332 333 334

  axiom Same_block_def:
    (forall p0:(pointer 'a1).
      (forall q0:(pointer 'a1).
        ((same_block p0 q0) <->
         ((base_block p0 : (block 'a1)) = (base_block q0 : (block 'a1))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
335
  function sub_pointer (pointer 'a1) (pointer 'a1) : int
François Bobot's avatar
François Bobot committed
336

Andrei Paskevich's avatar
Andrei Paskevich committed
337
  function shift (pointer 'a1) int : (pointer 'a1)
François Bobot's avatar
François Bobot committed
338

Andrei Paskevich's avatar
Andrei Paskevich committed
339
  function null  : (pointer 'a1)
François Bobot's avatar
François Bobot committed
340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401

  axiom Address_injective:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        ((p = q) <-> ((address p : int) = (address q : int)))))

  axiom Address_null: ((address (null : (pointer 'a1)) : int) = 0)

  axiom Address_positive:
    (forall p:(pointer 'a1). (Int.(<=) 0 (address p : int)))

  axiom Address_shift_lt:
    (forall p:(pointer 'a1).
      (forall i:int.
        (forall j:int [(address (shift p i : (pointer 'a1)) : int),
          (address (shift p j : (pointer 'a1)) : int)].
          ((Int.(<) (address (shift p i : (pointer 'a1)) : int) (address (shift p j : (pointer 'a1)) : int)) <->
           (Int.(<) i j)))))

  axiom Address_shift_le:
    (forall p:(pointer 'a1).
      (forall i:int.
        (forall j:int [(address (shift p i : (pointer 'a1)) : int),
          (address (shift p j : (pointer 'a1)) : int)].
          ((Int.(<=) (address (shift p i : (pointer 'a1)) : int) (address (shift p j : (pointer 'a1)) : int)) <->
           (Int.(<=) i j)))))

  axiom Shift_zero:
    (forall p:(pointer 'a1) [(shift p 0 : (pointer 'a1))].
      ((shift p 0 : (pointer 'a1)) = p))

  axiom Shift_shift:
    (forall p:(pointer 'a1).
      (forall i:int.
        (forall j:int [(shift (shift p i : (pointer 'a1)) j : (pointer 'a1))].
          ((shift (shift p i : (pointer 'a1)) j : (pointer 'a1)) = (shift p (Int.(+) i j : int) : (pointer 'a1))))))

  axiom Offset_max_shift:
    (forall a:(alloc_table 'a1).
      (forall p:(pointer 'a1).
        (forall i:int.
          ((offset_max a (shift p i : (pointer 'a1)) : int) = (Int.(-) (offset_max a p : int) i : int)))))

  axiom Offset_min_shift:
    (forall a:(alloc_table 'a1).
      (forall p:(pointer 'a1).
        (forall i:int.
          ((offset_min a (shift p i : (pointer 'a1)) : int) = (Int.(-) (offset_min a p : int) i : int)))))

  axiom Neq_shift:
    (forall p:(pointer 'a1).
      (forall i:int.
        (forall j:int [(shift p i : (pointer 'a1)),
          (shift p j : (pointer 'a1))].
          ((i <> j) ->
           ((shift p i : (pointer 'a1)) <> (shift p j : (pointer 'a1)))))))

  axiom Null_not_valid:
    (forall a:(alloc_table 'a1). (not (valid a (null : (pointer 'a1)))))

  axiom Null_pointer:
    (forall a:(alloc_table 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
402
      ((Int.(>=) (offset_min a (null : (pointer 'a1)) : int) 0) /\
François Bobot's avatar
François Bobot committed
403 404
       (Int.(<=) (offset_max a (null : (pointer 'a1)) : int) (Int.(-_) 2 : int))))

Andrei Paskevich's avatar
Andrei Paskevich committed
405
  function eq_pointer_bool (pointer 'a1) (pointer 'a1) : Bool.bool
François Bobot's avatar
François Bobot committed
406

Andrei Paskevich's avatar
Andrei Paskevich committed
407
  function neq_pointer_bool (pointer 'a1) (pointer 'a1) : Bool.bool
François Bobot's avatar
François Bobot committed
408 409 410 411

  axiom Eq_pointer_bool_def:
    (forall p1:(pointer 'a1).
      (forall p2:(pointer 'a1).
412
        (((eq_pointer_bool p1 p2 : Bool.bool) = Bool.ttrue) <-> (p1 = p2))))
François Bobot's avatar
François Bobot committed
413 414 415 416

  axiom Neq_pointer_bool_def:
    (forall p1:(pointer 'a1).
      (forall p2:(pointer 'a1).
417
        (((neq_pointer_bool p1 p2 : Bool.bool) = Bool.ttrue) <-> (p1 <> p2))))
François Bobot's avatar
François Bobot committed
418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457

  axiom Same_block_shift_right:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(same_block p (shift q i : (pointer 'a1)))].
          ((same_block p q) -> (same_block p (shift q i : (pointer 'a1)))))))

  axiom Same_block_shift_left:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(same_block (shift q i : (pointer 'a1)) p)].
          ((same_block q p) -> (same_block (shift q i : (pointer 'a1)) p)))))

  axiom Sub_pointer_shift:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1) [(sub_pointer p q : int)].
        ((same_block p q) ->
         (p = (shift q (sub_pointer p q : int) : (pointer 'a1))))))

  axiom Sub_pointer_self:
    (forall p:(pointer 'a1) [(sub_pointer p p : int)].
      ((sub_pointer p p : int) = 0))

  axiom Sub_pointer_zero:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1) [(sub_pointer p q : int)].
        ((same_block p q) -> (((sub_pointer p q : int) = 0) -> (p = q)))))

  axiom Sub_pointer_shift_left:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(sub_pointer (shift p i : (pointer 'a1)) q : int)].
          ((sub_pointer (shift p i : (pointer 'a1)) q : int) = (Int.(+) (sub_pointer p q : int) i : int)))))

  axiom Sub_pointer_shift_right:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(sub_pointer p (shift q i : (pointer 'a1)) : int)].
          ((sub_pointer p (shift q i : (pointer 'a1)) : int) = (Int.(-) (sub_pointer p q : int) i : int)))))

458
  type memory 't 'v = A.t (pointer 't) 'v
François Bobot's avatar
François Bobot committed
459

Andrei Paskevich's avatar
Andrei Paskevich committed
460
  function select (m:memory 'a1 'a2) (k:pointer 'a1) : 'a2 = A.get m k
François Bobot's avatar
François Bobot committed
461

Andrei Paskevich's avatar
Andrei Paskevich committed
462
  function store (m:memory 'a1 'a2) (k:pointer 'a1) (v:'a2) : (memory 'a1 'a2) = A.set m k v
François Bobot's avatar
François Bobot committed
463 464 465 466 467



  type pset 't

Andrei Paskevich's avatar
Andrei Paskevich committed
468
  function pset_empty  : (pset 'a1)
François Bobot's avatar
François Bobot committed
469

Andrei Paskevich's avatar
Andrei Paskevich committed
470
  function pset_singleton (pointer 'a1) : (pset 'a1)
François Bobot's avatar
François Bobot committed
471

Andrei Paskevich's avatar
Andrei Paskevich committed
472
  function pset_deref (memory 'a2 (pointer 'a1)) (pset 'a2) : (pset 'a1)
François Bobot's avatar
François Bobot committed
473

Andrei Paskevich's avatar
Andrei Paskevich committed
474
  function pset_union (pset 'a1) (pset 'a1) : (pset 'a1)
François Bobot's avatar
François Bobot committed
475

Andrei Paskevich's avatar
Andrei Paskevich committed
476
  function pset_all (pset 'a1) : (pset 'a1)
François Bobot's avatar
François Bobot committed
477

Andrei Paskevich's avatar
Andrei Paskevich committed
478
  function pset_range (pset 'a1) int int : (pset 'a1)
François Bobot's avatar
François Bobot committed
479

Andrei Paskevich's avatar
Andrei Paskevich committed
480
  function pset_range_left (pset 'a1) int : (pset 'a1)
François Bobot's avatar
François Bobot committed
481

Andrei Paskevich's avatar
Andrei Paskevich committed
482
  function pset_range_right (pset 'a1) int : (pset 'a1)
François Bobot's avatar
François Bobot committed
483

Andrei Paskevich's avatar
Andrei Paskevich committed
484
  predicate in_pset (pointer 'a1) (pset 'a1)
François Bobot's avatar
François Bobot committed
485

Andrei Paskevich's avatar
Andrei Paskevich committed
486
  predicate valid_pset (alloc_table 'a1) (pset 'a1)
François Bobot's avatar
François Bobot committed
487

Andrei Paskevich's avatar
Andrei Paskevich committed
488
  predicate pset_disjoint (pset 'a1) (pset 'a1)
François Bobot's avatar
François Bobot committed
489 490 491 492 493 494

  axiom Pset_disjoint_def:
    (forall ps1_0:(pset 'a1).
      (forall ps2_0:(pset 'a1).
        ((pset_disjoint ps1_0 ps2_0) <->
         (forall p:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
495
           (not ((in_pset p ps1_0) /\ (in_pset p ps2_0)))))))
François Bobot's avatar
François Bobot committed
496

Andrei Paskevich's avatar
Andrei Paskevich committed
497
  predicate pset_included (pset 'a1) (pset 'a1)
François Bobot's avatar
François Bobot committed
498 499 500 501 502 503 504 505 506 507 508 509 510 511 512

  axiom Pset_included_def:
    (forall ps1_0:(pset 'a1).
      (forall ps2_0:(pset 'a1).
        ((pset_included ps1_0 ps2_0) <->
         (forall p:(pointer 'a1). ((in_pset p ps1_0) -> (in_pset p ps2_0))))))

  axiom Pset_included_self: (forall ps:(pset 'a1). (pset_included ps ps))

  axiom Pset_included_range:
    (forall ps:(pset 'a1).
      (forall a:int.
        (forall b:int.
          (forall c:int.
            (forall d:int [(pset_included (pset_range ps a b : (pset 'a1)) (pset_range ps c d : (pset 'a1)))].
Andrei Paskevich's avatar
Andrei Paskevich committed
513
              (((Int.(<=) c a) /\ (Int.(<=) b d)) ->
François Bobot's avatar
François Bobot committed
514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537
               (pset_included (pset_range ps a b : (pset 'a1)) (pset_range ps c d : (pset 'a1)))))))))

  axiom Pset_included_range_all:
    (forall ps:(pset 'a1).
      (forall a:int.
        (forall b:int.
          (forall c:int.
            (forall d:int [(pset_included (pset_range ps a b : (pset 'a1)) (pset_range ps c d : (pset 'a1)))].
              (pset_included (pset_range ps a b : (pset 'a1)) (pset_all ps : (pset 'a1))))))))

  axiom In_pset_empty:
    (forall p:(pointer 'a1). (not (in_pset p (pset_empty : (pset 'a1)))))

  axiom In_pset_singleton:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        ((in_pset p (pset_singleton q : (pset 'a1))) <-> (p = q))))

  axiom In_pset_deref:
    (forall p:(pointer 'a1).
      (forall m:(memory 'a2 (pointer 'a1)).
        (forall q:(pset 'a2).
          ((in_pset p (pset_deref m q : (pset 'a1))) <->
           (exists r:(pointer 'a2).
Andrei Paskevich's avatar
Andrei Paskevich committed
538
             ((in_pset r q) /\ (p = (select m r : (pointer 'a1)))))))))
François Bobot's avatar
François Bobot committed
539 540 541 542 543 544 545

  axiom In_pset_all:
    (forall p:(pointer 'a1).
      (forall q:(pset 'a1).
        ((in_pset p (pset_all q : (pset 'a1))) <->
         (exists i:int.
           (exists r:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
546
             ((in_pset r q) /\ (p = (shift r i : (pointer 'a1)))))))))
François Bobot's avatar
François Bobot committed
547 548 549 550 551 552 553 554 555

  axiom In_pset_range:
    (forall p:(pointer 'a1).
      (forall q:(pset 'a1).
        (forall a:int.
          (forall b:int.
            ((in_pset p (pset_range q a b : (pset 'a1))) <->
             (exists i:int.
               (exists r:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
556 557 558
                 ((Int.(<=) a i) /\
                  ((Int.(<=) i b) /\
                   ((in_pset r q) /\ (p = (shift r i : (pointer 'a1)))))))))))))
François Bobot's avatar
François Bobot committed
559 560 561 562 563 564 565 566

  axiom In_pset_range_left:
    (forall p:(pointer 'a1).
      (forall q:(pset 'a1).
        (forall b:int.
          ((in_pset p (pset_range_left q b : (pset 'a1))) <->
           (exists i:int.
             (exists r:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
567 568
               ((Int.(<=) i b) /\
                ((in_pset r q) /\ (p = (shift r i : (pointer 'a1)))))))))))
François Bobot's avatar
François Bobot committed
569 570 571 572 573 574 575 576

  axiom In_pset_range_right:
    (forall p:(pointer 'a1).
      (forall q:(pset 'a1).
        (forall a:int.
          ((in_pset p (pset_range_right q a : (pset 'a1))) <->
           (exists i:int.
             (exists r:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
577 578
               ((Int.(<=) a i) /\
                ((in_pset r q) /\ (p = (shift r i : (pointer 'a1)))))))))))
François Bobot's avatar
François Bobot committed
579 580 581 582 583 584

  axiom In_pset_union:
    (forall p:(pointer 'a1).
      (forall s1:(pset 'a1).
        (forall s2:(pset 'a1).
          ((in_pset p (pset_union s1 s2 : (pset 'a1))) <->
Andrei Paskevich's avatar
Andrei Paskevich committed
585
           ((in_pset p s1) \/ (in_pset p s2))))))
François Bobot's avatar
François Bobot committed
586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601

  axiom Valid_pset_empty:
    (forall a:(alloc_table 'a1). (valid_pset a (pset_empty : (pset 'a1))))

  axiom Valid_pset_singleton:
    (forall a:(alloc_table 'a1).
      (forall p:(pointer 'a1).
        ((valid_pset a (pset_singleton p : (pset 'a1))) <-> (valid a p))))

  axiom Valid_pset_deref:
    (forall a:(alloc_table 'a1).
      (forall m:(memory 'a2 (pointer 'a1)).
        (forall q:(pset 'a2).
          ((valid_pset a (pset_deref m q : (pset 'a1))) <->
           (forall r:(pointer 'a2).
             (forall p:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
602
               (((in_pset r q) /\ (p = (select m r : (pointer 'a1)))) ->
François Bobot's avatar
François Bobot committed
603 604 605 606 607 608 609 610 611 612
                (valid a p))))))))

  axiom Valid_pset_range:
    (forall a:(alloc_table 'a1).
      (forall q:(pset 'a1).
        (forall c:int.
          (forall d:int.
            ((valid_pset a (pset_range q c d : (pset 'a1))) <->
             (forall i:int.
               (forall r:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
613
                 (((in_pset r q) /\ ((Int.(<=) c i) /\ (Int.(<=) i d))) ->
François Bobot's avatar
François Bobot committed
614 615 616 617 618 619 620
                  (valid a (shift r i : (pointer 'a1)))))))))))

  axiom Valid_pset_union:
    (forall a:(alloc_table 'a1).
      (forall s1:(pset 'a1).
        (forall s2:(pset 'a1).
          ((valid_pset a (pset_union s1 s2 : (pset 'a1))) <->
Andrei Paskevich's avatar
Andrei Paskevich committed
621
           ((valid_pset a s1) /\ (valid_pset a s2))))))
François Bobot's avatar
François Bobot committed
622

Andrei Paskevich's avatar
Andrei Paskevich committed
623
  predicate not_assigns (alloc_table 'a1) (memory 'a1 'a2) (memory 'a1 'a2) (pset 'a1)
François Bobot's avatar
François Bobot committed
624 625 626 627 628 629 630 631

  axiom Not_assigns_def:
    (forall a0:(alloc_table 'a1).
      (forall m1_0:(memory 'a1 'a2).
        (forall m2_0:(memory 'a1 'a2).
          (forall l0:(pset 'a1).
            ((not_assigns a0 m1_0 m2_0 l0) <->
             (forall p:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
632
               (((valid a0 p) /\ (not (in_pset p l0))) ->
François Bobot's avatar
François Bobot committed
633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649
                ((select m2_0 p : 'a2) = (select m1_0 p : 'a2)))))))))

  axiom Not_assigns_refl:
    (forall a:(alloc_table 'a1).
      (forall m:(memory 'a1 'a2).
        (forall l:(pset 'a1). (not_assigns a m m l))))

  axiom Not_assigns_trans:
    (forall a:(alloc_table 'a1).
      (forall m1:(memory 'a1 'a2).
        (forall m2:(memory 'a1 'a2).
          (forall m3:(memory 'a1 'a2).
            (forall l:(pset 'a1) [(not_assigns a m1 m2 l),
              (not_assigns a m1 m3 l)].
              ((not_assigns a m1 m2 l) ->
               ((not_assigns a m2 m3 l) -> (not_assigns a m1 m3 l))))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
650
  predicate full_separated (pointer 'a1) (pointer 'a2)
François Bobot's avatar
François Bobot committed
651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683

  axiom Full_separated_shift1:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(full_separated p q), (shift q i : (pointer 'a1))].
          ((full_separated p q) ->
           (full_separated p (shift q i : (pointer 'a1)))))))

  axiom Full_separated_shift2:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(full_separated p q), (shift q i : (pointer 'a1))].
          ((full_separated p q) ->
           (full_separated (shift q i : (pointer 'a1)) p)))))

  axiom Full_separated_shift3:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(full_separated q p), (shift q i : (pointer 'a1))].
          ((full_separated q p) ->
           (full_separated (shift q i : (pointer 'a1)) p)))))

  axiom Full_separated_shift4:
    (forall p:(pointer 'a1).
      (forall q:(pointer 'a1).
        (forall i:int [(full_separated q p), (shift q i : (pointer 'a1))].
          ((full_separated q p) ->
           (full_separated p (shift q i : (pointer 'a1)))))))

  type tag_table 't

  type tag_id 't

Andrei Paskevich's avatar
Andrei Paskevich committed
684
  function int_of_tag (tag_id 'a1) : int
François Bobot's avatar
François Bobot committed
685

Andrei Paskevich's avatar
Andrei Paskevich committed
686
  function typeof (tag_table 'a1) (pointer 'a1) : (tag_id 'a1)
François Bobot's avatar
François Bobot committed
687

Andrei Paskevich's avatar
Andrei Paskevich committed
688
  predicate parenttag (tag_id 'a1) (tag_id 'a1)
François Bobot's avatar
François Bobot committed
689

Andrei Paskevich's avatar
Andrei Paskevich committed
690
  predicate subtag (tag_id 'a1) (tag_id 'a1)
François Bobot's avatar
François Bobot committed
691

Andrei Paskevich's avatar
Andrei Paskevich committed
692
  function subtag_bool (tag_id 'a1) (tag_id 'a1) : Bool.bool
François Bobot's avatar
François Bobot committed
693 694 695 696

  axiom Subtag_bool_def:
    (forall t1:(tag_id 'a1).
      (forall t2:(tag_id 'a1).
697
        (((subtag_bool t1 t2 : Bool.bool) = Bool.ttrue) <-> (subtag t1 t2))))
François Bobot's avatar
François Bobot committed
698 699 700 701 702 703 704 705 706

  axiom Subtag_refl: (forall t:(tag_id 'a1). (subtag t t))

  axiom Subtag_parent:
    (forall t1:(tag_id 'a1).
      (forall t2:(tag_id 'a1).
        (forall t3:(tag_id 'a1).
          ((subtag t1 t2) -> ((parenttag t2 t3) -> (subtag t1 t3))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
707
  predicate instanceof (tag_table 'a1) (pointer 'a1) (tag_id 'a1)
François Bobot's avatar
François Bobot committed
708 709 710 711 712 713 714 715

  axiom Instanceof_def:
    (forall a0:(tag_table 'a1).
      (forall p0:(pointer 'a1).
        (forall t0:(tag_id 'a1).
          ((instanceof a0 p0 t0) <->
           (subtag (typeof a0 p0 : (tag_id 'a1)) t0)))))

Andrei Paskevich's avatar
Andrei Paskevich committed
716
  function downcast (tag_table 'a1) (pointer 'a1) (tag_id 'a1) : (pointer 'a1)
François Bobot's avatar
François Bobot committed
717 718 719 720 721 722 723

  axiom Downcast_instanceof:
    (forall a:(tag_table 'a1).
      (forall p:(pointer 'a1).
        (forall s:(tag_id 'a1).
          ((instanceof a p s) -> ((downcast a p s : (pointer 'a1)) = p)))))

Andrei Paskevich's avatar
Andrei Paskevich committed
724
  function bottom_tag  : (tag_id 'a1)
François Bobot's avatar
François Bobot committed
725 726 727 728

  axiom Bottom_tag_axiom:
    (forall t:(tag_id 'a1). (subtag t (bottom_tag : (tag_id 'a1))))

Andrei Paskevich's avatar
Andrei Paskevich committed
729
  predicate root_tag (tag_id 'a1)
François Bobot's avatar
François Bobot committed
730 731 732 733 734 735 736 737 738 739 740 741 742

  axiom Root_tag_def:
    (forall t0:(tag_id 'a1).
      ((root_tag t0) <-> (parenttag t0 (bottom_tag : (tag_id 'a1)))))

  axiom Root_subtag:
    (forall a:(tag_id 'a1).
      (forall b:(tag_id 'a1).
        (forall c:(tag_id 'a1).
          ((root_tag a) ->
           ((root_tag b) ->
            ((a <> b) -> ((subtag c a) -> (not (subtag c b)))))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
743
  predicate fully_packed (tag_table 'a1) (memory 'a1 (tag_id 'a1)) (pointer 'a1)
François Bobot's avatar
François Bobot committed
744 745 746 747 748 749 750 751

  axiom Fully_packed_def:
    (forall tag_table0:(tag_table 'a1).
      (forall mutable0:(memory 'a1 (tag_id 'a1)).
        (forall this0:(pointer 'a1).
          ((fully_packed tag_table0 mutable0 this0) <->
           ((select mutable0 this0 : (tag_id 'a1)) = (typeof tag_table0 this0 : (tag_id 'a1)))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
752
  function bw_compl int : int
François Bobot's avatar
François Bobot committed
753

Andrei Paskevich's avatar
Andrei Paskevich committed
754
  function bw_and int int : int
François Bobot's avatar
François Bobot committed
755 756 757

  axiom Bw_and_not_null:
    (forall a:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
758
      (forall b:int. (((bw_and a b : int) <> 0) -> ((a <> 0) /\ (b <> 0)))))
François Bobot's avatar
François Bobot committed
759

Andrei Paskevich's avatar
Andrei Paskevich committed
760
  function bw_xor int int : int
François Bobot's avatar
François Bobot committed
761

Andrei Paskevich's avatar
Andrei Paskevich committed
762
  function bw_or int int : int
François Bobot's avatar
François Bobot committed
763

Andrei Paskevich's avatar
Andrei Paskevich committed
764
  function lsl int int : int
François Bobot's avatar
François Bobot committed
765 766 767 768

  axiom Lsl_left_positive_returns_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
769
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) 0 (lsl a b : int)))))
François Bobot's avatar
François Bobot committed
770 771 772 773 774

  axiom Lsl_left_positive_monotone:
    (forall a1:int.
      (forall a2:int.
        (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
775
          (((Int.(<=) 0 a1) /\ ((Int.(<=) a1 a2) /\ (Int.(<=) 0 b))) ->
François Bobot's avatar
François Bobot committed
776 777
           (Int.(<=) (lsl a1 b : int) (lsl a2 b : int))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
778
  function lsr int int : int
François Bobot's avatar
François Bobot committed
779 780 781 782

  axiom Lsr_left_positive_returns_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
783
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) 0 (lsr a b : int)))))
François Bobot's avatar
François Bobot committed
784 785 786 787

  axiom Lsr_left_positive_decreases:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
788
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) (lsr a b : int) a))))
François Bobot's avatar
François Bobot committed
789

Andrei Paskevich's avatar
Andrei Paskevich committed
790
  function asr int int : int
François Bobot's avatar
François Bobot committed
791 792 793 794

  axiom Asr_positive_on_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
795
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) 0 (asr a b : int)))))
François Bobot's avatar
François Bobot committed
796 797 798 799

  axiom Asr_decreases_on_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
800
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) (asr a b : int) a))))
François Bobot's avatar
François Bobot committed
801 802 803 804

  axiom Asr_lsr_same_on_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
805
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) ->
François Bobot's avatar
François Bobot committed
806 807 808 809 810
         ((asr a b : int) = (lsr a b : int)))))

  axiom Lsl_of_lsr_decreases_on_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
811
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) ->
François Bobot's avatar
François Bobot committed
812 813 814 815 816
         (Int.(<=) (lsl (lsr a b : int) b : int) a))))

  axiom Lsr_of_lsl_identity_on_positive:
    (forall a:int.
      (forall b:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
817
        (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) ->
François Bobot's avatar
François Bobot committed
818 819
         ((lsr (lsl a b : int) b : int) = a))))

Andrei Paskevich's avatar
Andrei Paskevich committed
820
  predicate alloc_extends (alloc_table 'a1) (alloc_table 'a1)
François Bobot's avatar
François Bobot committed
821

Andrei Paskevich's avatar
Andrei Paskevich committed
822
  predicate alloc_fresh (alloc_table 'a1) (pointer 'a1) int
François Bobot's avatar
François Bobot committed
823 824 825 826 827 828 829

  axiom Alloc_fresh_def:
    (forall a0:(alloc_table 'a1).
      (forall p0:(pointer 'a1).
        (forall n0:int.
          ((alloc_fresh a0 p0 n0) <->
           (forall i:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
830
             (((Int.(<=) 0 i) /\ (Int.(<) i n0)) ->
François Bobot's avatar
François Bobot committed
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857
              (not (valid a0 (shift p0 i : (pointer 'a1))))))))))

  axiom Alloc_extends_offset_min:
    (forall a1:(alloc_table 'a1).
      (forall a2:(alloc_table 'a1) [(alloc_extends a1 a2)].
        ((alloc_extends a1 a2) ->
         (forall p:(pointer 'a1).
           ((valid a1 p) ->
            ((offset_min a1 p : int) = (offset_min a2 p : int)))))))

  axiom Alloc_extends_offset_max:
    (forall a1:(alloc_table 'a1).
      (forall a2:(alloc_table 'a1) [(alloc_extends a1 a2)].
        ((alloc_extends a1 a2) ->
         (forall p:(pointer 'a1).
           ((valid a1 p) ->
            ((offset_max a1 p : int) = (offset_max a2 p : int)))))))

  axiom Alloc_extends_not_assigns_empty:
    (forall a1:(alloc_table 'a1).
      (forall a2:(alloc_table 'a1).
        (forall m1:(memory 'a1 'a2).
          (forall m2:(memory 'a1 'a2).
            (forall l:(pset 'a1).
              (forall p:(pointer 'a1).
                (forall n:int [(alloc_extends a1 a2), (alloc_fresh a1 p n),
                  (not_assigns a2 m1 m2 l)].
Andrei Paskevich's avatar
Andrei Paskevich committed
858 859 860
                  (((alloc_extends a1 a2) /\
                    ((alloc_fresh a1 p n) /\
                     ((not_assigns a2 m1 m2 l) /\
François Bobot's avatar
François Bobot committed
861 862 863
                      (pset_included l (pset_all (pset_singleton p : (pset 'a1)) : (pset 'a1)))))) ->
                   (not_assigns a1 m1 m2 (pset_empty : (pset 'a1)))))))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
864
  predicate alloc_extends_except (alloc_table 'a1) (alloc_table 'a1) (pset 'a1)
François Bobot's avatar
François Bobot committed
865 866 867 868 869 870 871

  axiom Alloc_extends_except_offset_min:
    (forall a1:(alloc_table 'a1).
      (forall a2:(alloc_table 'a1).
        (forall l:(pset 'a1) [(alloc_extends_except a1 a2 l)].
          ((alloc_extends_except a1 a2 l) ->
           (forall p:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
872
             (((valid a1 p) /\ (not (in_pset p l))) ->
François Bobot's avatar
François Bobot committed
873 874 875 876 877 878 879 880
              ((offset_min a1 p : int) = (offset_min a2 p : int))))))))

  axiom Alloc_extends_except_offset_max:
    (forall a1:(alloc_table 'a1).
      (forall a2:(alloc_table 'a1).
        (forall l:(pset 'a1) [(alloc_extends_except a1 a2 l)].
          ((alloc_extends_except a1 a2 l) ->
           (forall p:(pointer 'a1).
Andrei Paskevich's avatar
Andrei Paskevich committed
881
             (((valid a1 p) /\ (not (in_pset p l))) ->
François Bobot's avatar
François Bobot committed
882 883 884 885
              ((offset_max a1 p : int) = (offset_max a2 p : int))))))))

  type bitvector

Andrei Paskevich's avatar
Andrei Paskevich committed
886
  function concat_bitvector bitvector bitvector : bitvector
François Bobot's avatar
François Bobot committed
887

Andrei Paskevich's avatar
Andrei Paskevich committed
888
  function offset_min_bytes (alloc_table 'a1) (pointer 'a1) int : int
François Bobot's avatar
François Bobot committed
889

Andrei Paskevich's avatar
Andrei Paskevich committed
890
  function offset_max_bytes (alloc_table 'a1) (pointer 'a1) int : int
François Bobot's avatar
François Bobot committed
891 892 893 894 895 896

  axiom Offset_min_bytes_def:
    (forall a:(alloc_table 'a1).
      (forall p:(pointer 'a1).
        (forall s:int [(offset_min_bytes a p s : int)].
          ((Int.(<) 0 s) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
897
           ((Int.(<=) (offset_min a p : int) (Int.(*) s (offset_min_bytes a p s : int) : int)) /\
François Bobot's avatar
François Bobot committed
898 899 900 901 902 903 904
            (Int.(<) (Int.(-) (Int.(*) s (offset_min_bytes a p s : int) : int) s : int) (offset_min a p : int)))))))

  axiom Offset_max_bytes_def:
    (forall a:(alloc_table 'a1).
      (forall p:(pointer 'a1).
        (forall s:int [(offset_max_bytes a p s : int)].
          ((Int.(<) 0 s) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
905
           ((Int.(<=) (Int.(-) (Int.(+) (Int.(*) s (offset_max_bytes a p s : int) : int) s : int) 1 : int) (offset_max a p : int)) /\
François Bobot's avatar
François Bobot committed
906 907
            (Int.(<) (offset_max a p : int) (Int.(-) (Int.(+) (Int.(+) (Int.(*) s (offset_max_bytes a p s : int) : int) s : int) s : int) 1 : int)))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
908
  function extract_bytes bitvector int int : bitvector
François Bobot's avatar
François Bobot committed
909

Andrei Paskevich's avatar
Andrei Paskevich committed
910
  function replace_bytes bitvector int int bitvector : bitvector
François Bobot's avatar
François Bobot committed
911 912 913 914 915 916 917 918

  axiom Select_store_eq_union:
    (forall o1:int.
      (forall s1:int.
        (forall o2:int.
          (forall s2:int.
            (forall v1:bitvector.
              (forall v2:bitvector [(extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector)].
Andrei Paskevich's avatar
Andrei Paskevich committed
919
                (((o1 = o2) /\ (s1 = s2)) ->
François Bobot's avatar
François Bobot committed
920 921 922 923 924 925 926 927 928
                 ((extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector) = v2))))))))

  axiom Select_store_neq_union:
    (forall o1:int.
      (forall s1:int.
        (forall o2:int.
          (forall s2:int.
            (forall v1:bitvector.
              (forall v2:bitvector [(extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector)].
Andrei Paskevich's avatar
Andrei Paskevich committed
929
                (((Int.(<=) (Int.(+) o2 s2 : int) o1) \/
François Bobot's avatar
François Bobot committed
930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963
                  (Int.(<=) (Int.(+) o1 s2 : int) o2)) ->
                 ((extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector) = (extract_bytes v1 o2 s2 : bitvector)))))))))

  axiom Concat_replace_bytes_up:
    (forall o1:int.
      (forall s1:int.
        (forall o2:int.
          (forall s2:int.
            (forall v1:bitvector.
              (forall v2:bitvector.
                (forall v3:bitvector [(replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector)].
                  (((Int.(+) o1 s1 : int) = o2) ->
                   ((replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector) = (replace_bytes v1 o1 (Int.(+) s1 s2 : int) (concat_bitvector v2 v3 : bitvector) : bitvector))))))))))

  axiom Concat_replace_bytes_down:
    (forall o1:int.
      (forall s1:int.
        (forall o2:int.
          (forall s2:int.
            (forall v1:bitvector.
              (forall v2:bitvector.
                (forall v3:bitvector [(replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector)].
                  (((Int.(+) o2 s2 : int) = o1) ->
                   ((replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector) = (replace_bytes v1 o2 (Int.(+) s1 s2 : int) (concat_bitvector v3 v2 : bitvector) : bitvector))))))))))

  axiom Concat_extract_bytes:
    (forall o1:int.
      (forall s1:int.
        (forall o2:int.
          (forall s2:int.
            (forall v:bitvector [(concat_bitvector (extract_bytes v o1 s1 : bitvector) (extract_bytes v o2 s2 : bitvector) : bitvector)].
              (((Int.(+) o1 s1 : int) = o2) ->
               ((concat_bitvector (extract_bytes v o1 s1 : bitvector) (extract_bytes v o2 s2 : bitvector) : bitvector) = (extract_bytes v o1 (Int.(+) s1 s2 : int) : bitvector))))))))

Andrei Paskevich's avatar
Andrei Paskevich committed
964
  function select_bytes (memory 'a1 bitvector) (pointer 'a1) int int : bitvector
François Bobot's avatar
François Bobot committed
965

Andrei Paskevich's avatar
Andrei Paskevich committed
966
  function store_bytes (memory 'a1 bitvector) (pointer 'a1) int int bitvector : (memory 'a1 bitvector)
François Bobot's avatar
François Bobot committed
967 968 969 970 971 972 973 974 975 976

  axiom Select_store_eq_bytes:
    (forall m:(memory 'a1 bitvector).
      (forall p1:(pointer 'a1).
        (forall p2:(pointer 'a1).
          (forall o1:int.
            (forall s1:int.
              (forall o2:int.
                (forall s2:int.
                  (forall v:bitvector [(select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector)].
Andrei Paskevich's avatar
Andrei Paskevich committed
977
                    (((p1 = p2) /\ ((o1 = o2) /\ (s1 = s2))) ->
François Bobot's avatar
François Bobot committed
978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053
                     ((select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector) = v))))))))))

  axiom Select_store_neq_bytes:
    (forall m:(memory 'a1 bitvector).
      (forall p1:(pointer 'a1).
        (forall p2:(pointer 'a1).
          (forall o1:int.
            (forall s1:int.
              (forall o2:int.
                (forall s2:int.
                  (forall v:bitvector [(select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector)].
                    ((pset_disjoint (pset_range (pset_singleton p1 : (pset 'a1)) o1 (Int.(+) o1 s1 : int) : (pset 'a1)) (pset_range (pset_singleton p2 : (pset 'a1)) o2 (Int.(+) o2 s2 : int) : (pset 'a1))) ->
                     ((select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector) = (select_bytes m p2 o2 s2 : bitvector)))))))))))

  axiom Shift_store_bytes:
    (forall m:(memory 'a1 bitvector).
      (forall p:(pointer 'a1).
        (forall i:int.
          (forall o:int.
            (forall s:int.
              (forall v:bitvector [(store_bytes m (shift p i : (pointer 'a1)) o s v : (memory 'a1 bitvector))].
                ((store_bytes m (shift p i : (pointer 'a1)) o s v : (memory 'a1 bitvector)) = (store_bytes m p (Int.(+) o i : int) s v : (memory 'a1 bitvector)))))))))

  axiom Shift_select_bytes:
    (forall m:(memory 'a1 bitvector).
      (forall p:(pointer 'a1).
        (forall i:int.
          (forall o:int.
            (forall s:int.
              (forall v:bitvector [(select_bytes m (shift p i : (pointer 'a1)) o s : bitvector)].
                ((select_bytes m (shift p i : (pointer 'a1)) o s : bitvector) = (select_bytes m p (Int.(+) o i : int) s : bitvector))))))))

  axiom Concat_store_bytes_up:
    (forall m:(memory 'a1 bitvector).
      (forall p:(pointer 'a1).
        (forall o1:int.
          (forall s1:int.
            (forall o2:int.
              (forall s2:int.
                (forall v1:bitvector.
                  (forall v2:bitvector [(store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector))].
                    (((Int.(+) o1 s1 : int) = o2) ->
                     ((store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector)) = (store_bytes m p o1 (Int.(+) s1 s2 : int) (concat_bitvector v1 v2 : bitvector) : (memory 'a1 bitvector))))))))))))

  axiom Concat_store_bytes_down:
    (forall m:(memory 'a1 bitvector).
      (forall p:(pointer 'a1).
        (forall o1:int.
          (forall s1:int.
            (forall o2:int.
              (forall s2:int.
                (forall v1:bitvector.
                  (forall v2:bitvector [(store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector))].
                    (((Int.(+) o2 s2 : int) = o1) ->
                     ((store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector)) = (store_bytes m p o2 (Int.(+) s1 s2 : int) (concat_bitvector v2 v1 : bitvector) : (memory 'a1 bitvector))))))))))))

  axiom Concat_select_bytes:
    (forall m:(memory 'a1 bitvector).
      (forall p:(pointer 'a1).
        (forall o1:int.
          (forall s1:int.
            (forall o2:int.
              (forall s2:int [(concat_bitvector (select_bytes m p o1 s1 : bitvector) (select_bytes m p o2 s2 : bitvector) : bitvector)].
                (((Int.(+) o1 s1 : int) = o2) ->
                 ((concat_bitvector (select_bytes m p o1 s1 : bitvector) (select_bytes m p o2 s2 : bitvector) : bitvector) = (select_bytes m p o1 (Int.(+) s1 s2 : int) : bitvector)))))))))

  type char_P

  type mybag

  type node

  type padding

  type void_P

Andrei Paskevich's avatar
Andrei Paskevich committed
1054
  predicate mybag_add (pointer node) mybag mybag
François Bobot's avatar
François Bobot committed
1055

Andrei Paskevich's avatar
Andrei Paskevich committed
1056
  predicate in_mybag (pointer node) mybag
François Bobot's avatar
François Bobot committed
1057 1058 1059 1060 1061 1062 1063

  axiom U_mybag_add:
    (forall s_1:mybag.
      (forall t_0:mybag.
        (forall p_3:(pointer node).
          ((mybag_add p_3 t_0 s_1) <->
           (forall n_1:(pointer node).
Andrei Paskevich's avatar
Andrei Paskevich committed
1064
             ((in_mybag n_1 s_1) <-> ((n_1 = p_3) \/ (in_mybag n_1 t_0))))))))
François Bobot's avatar
François Bobot committed
1065

Andrei Paskevich's avatar
Andrei Paskevich committed
1066
  function mybag_all  : mybag
François Bobot's avatar
François Bobot committed
1067 1068 1069 1070

  axiom U_mybag_all:
    (forall p_2_0:(pointer node). (in_mybag p_2_0 (mybag_all : mybag)))

Andrei Paskevich's avatar
Andrei Paskevich committed
1071
  function mybag_empty  : mybag
François Bobot's avatar
François Bobot committed
1072 1073 1074 1075 1076

  axiom U_mybag_empty:
    (forall p_1_0:(pointer node).
      (not (in_mybag p_1_0 (mybag_empty : mybag))))

Andrei Paskevich's avatar
Andrei Paskevich committed
1077
  predicate mybag_rem (pointer node) mybag mybag
François Bobot's avatar
François Bobot committed
1078 1079 1080 1081 1082 1083 1084 1085

  axiom U_mybag_rem:
    (forall s_3:mybag.
      (forall t_2:mybag.
        (forall p_4:(pointer node).
          ((mybag_rem p_4 t_2 s_3) <->
           (forall n_0_0:(pointer node).
             ((in_mybag n_0_0 s_3) <->
Andrei Paskevich's avatar
Andrei Paskevich committed
1086
              ((n_0_0 <> p_4) /\ (in_mybag n_0_0 t_2))))))))
François Bobot's avatar
François Bobot committed
1087

Andrei Paskevich's avatar
Andrei Paskevich committed
1088
  function bitvector_of_char_P (pointer char_P) : bitvector
François Bobot's avatar
François Bobot committed
1089

Andrei Paskevich's avatar
Andrei Paskevich committed
1090
  function char_P_of_bitvector bitvector : (pointer char_P)
François Bobot's avatar
François Bobot committed
1091 1092 1093 1094 1095

  axiom Bitvector_of_char_P_of_char_P_of_bitvector:
    (forall x:bitvector.
      ((bitvector_of_char_P (char_P_of_bitvector x : (pointer char_P)) : bitvector) = x))

Andrei Paskevich's avatar
Andrei Paskevich committed
1096
  function bitvector_of_node (pointer node) : bitvector
François Bobot's avatar
François Bobot committed
1097

Andrei Paskevich's avatar
Andrei Paskevich committed
1098
  function node_of_bitvector bitvector : (pointer node)
François Bobot's avatar
François Bobot committed
1099 1100 1101 1102 1103

  axiom Bitvector_of_node_of_node_of_bitvector:
    (forall x:bitvector.
      ((bitvector_of_node (node_of_bitvector x : (pointer node)) : bitvector) = x))

Andrei Paskevich's avatar
Andrei Paskevich committed
1104
  function bitvector_of_void_P (pointer void_P) : bitvector
François Bobot's avatar
François Bobot committed
1105

Andrei Paskevich's avatar
Andrei Paskevich committed
1106
  function void_P_of_bitvector bitvector : (pointer void_P)
François Bobot's avatar
François Bobot committed
1107 1108 1109 1110 1111

  axiom Bitvector_of_void_P_of_void_P_of_bitvector:
    (forall x:bitvector.
      ((bitvector_of_void_P (void_P_of_bitvector x : (pointer void_P)) : bitvector) = x))

Andrei Paskevich's avatar
Andrei Paskevich committed
1112
  function char_P_tag  : (tag_id char_P)
François Bobot's avatar
François Bobot committed
1113 1114 1115 1116 1117 1118 1119

  axiom Char_P_int: ((int_of_tag (char_P_tag : (tag_id char_P)) : int) = 1)

  axiom Char_P_of_bitvector_of_bitvector_of_char_P:
    (forall x:(pointer char_P).
      ((char_P_of_bitvector (bitvector_of_char_P x : bitvector) : (pointer char_P)) = x))

Andrei Paskevich's avatar
Andrei Paskevich committed
1120
  function char_P_of_pointer_address (pointer Unit.unit) : (pointer char_P)
François Bobot's avatar
François Bobot committed
1121 1122 1123

  axiom Char_P_of_pointer_address_of_pointer_addr:
    (forall p:(pointer char_P).
1124
      (p = (char_P_of_pointer_address (pointer_address p : (pointer Unit.unit)) : (pointer char_P))))
François Bobot's avatar
François Bobot committed
1125 1126 1127 1128 1129 1130 1131 1132 1133

  axiom Char_P_parenttag_bottom:
    (parenttag (char_P_tag : (tag_id char_P)) (bottom_tag : (tag_id char_P)))

  axiom Char_P_tags:
    (forall x:(pointer char_P).
      (forall char_P_tag_table:(tag_table char_P).
        (instanceof char_P_tag_table x (char_P_tag : (tag_id char_P)))))

Andrei Paskevich's avatar
Andrei Paskevich committed
1134
  predicate ilist (pointer node) (alloc_table node) (memory node (pointer node))
François Bobot's avatar
François Bobot committed
1135 1136 1137 1138 1139 1140 1141 1142

  axiom Ilist_inversion:
    (forall aux_1_0:(pointer node).
      (forall aux_2_0:(alloc_table node).
        (forall aux_3_0:(memory node (pointer node)).
          ((ilist aux_1_0 aux_2_0 aux_3_0) ->
           ((exists node_alloc_table_at_L:(alloc_table node).
              (exists node_tl_at_L:(memory node (pointer node)).
Andrei Paskevich's avatar
Andrei Paskevich committed
1143 1144 1145
                ((aux_1_0 = (null : (pointer node))) /\
                 ((aux_2_0 = node_alloc_table_at_L) /\
                  (aux_3_0 = node_tl_at_L))))) \/
François Bobot's avatar
François Bobot committed
1146 1147 1148
            (exists node_alloc_table_at_L:(alloc_table node).
              (exists node_tl_at_L:(memory node (pointer node)).
                (exists p_0_0:(pointer node).
Andrei Paskevich's avatar
Andrei Paskevich committed
1149 1150 1151 1152 1153 1154
                  ((p_0_0 <> (null : (pointer node))) /\
                   (((Int.(<=) (offset_min node_alloc_table_at_L p_0_0 : int) 0) /\
                     (Int.(>=) (offset_max node_alloc_table_at_L p_0_0 : int) 0)) /\
                    ((ilist (select node_tl_at_L p_0_0 : (pointer node)) node_alloc_table_at_L node_tl_at_L) /\
                     ((aux_1_0 = p_0_0) /\
                      ((aux_2_0 = node_alloc_table_at_L) /\
François Bobot's avatar
François Bobot committed
1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166
                       (aux_3_0 = node_tl_at_L))))))))))))))

  axiom Nil:
    (forall node_alloc_table_at_L:(alloc_table node).
      (forall node_tl_at_L:(memory node (pointer node)).
        (ilist (null : (pointer node)) node_alloc_table_at_L node_tl_at_L)))

  axiom Cons:
    (forall node_alloc_table_at_L:(alloc_table node).
      (forall node_tl_at_L:(memory node (pointer node)).
        (forall p_0_0:(pointer node).
          ((p_0_0 <> (null : (pointer node))) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
1167
           (((Int.(<=) (offset_min node_alloc_table_at_L p_0_0 : int) 0) /\
François Bobot's avatar
François Bobot committed
1168 1169 1170 1171
             (Int.(>=) (offset_max node_alloc_table_at_L p_0_0 : int) 0)) ->
            ((ilist (select node_tl_at_L p_0_0 : (pointer node)) node_alloc_table_at_L node_tl_at_L) ->
             (ilist p_0_0 node_alloc_table_at_L node_tl_at_L)))))))