source: driver/extracted/smallstep.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 16.7 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open Extralib
12
13open Lists
14
15open Identifiers
16
17open Integers
18
19open AST
20
21open Division
22
23open Exp
24
25open Arithmetic
26
27open Extranat
28
29open Vector
30
31open FoldStuff
32
33open BitVector
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
41open ErrorMessages
42
43open Option
44
45open Setoids
46
47open Monad
48
49open Positive
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open Events
86
87type transrel =
88| Mk_transrel
89
90(** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
91let rec transrel_rect_Type4 h_mk_transrel = function
92| Mk_transrel -> h_mk_transrel __ __ __
93
94(** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
95let rec transrel_rect_Type5 h_mk_transrel = function
96| Mk_transrel -> h_mk_transrel __ __ __
97
98(** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
99let rec transrel_rect_Type3 h_mk_transrel = function
100| Mk_transrel -> h_mk_transrel __ __ __
101
102(** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
103let rec transrel_rect_Type2 h_mk_transrel = function
104| Mk_transrel -> h_mk_transrel __ __ __
105
106(** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
107let rec transrel_rect_Type1 h_mk_transrel = function
108| Mk_transrel -> h_mk_transrel __ __ __
109
110(** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
111let rec transrel_rect_Type0 h_mk_transrel = function
112| Mk_transrel -> h_mk_transrel __ __ __
113
114type genv = __
115
116type state = __
117
118(** val transrel_inv_rect_Type4 :
119    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
120let transrel_inv_rect_Type4 hterm h1 =
121  let hcut = transrel_rect_Type4 h1 hterm in hcut __
122
123(** val transrel_inv_rect_Type3 :
124    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
125let transrel_inv_rect_Type3 hterm h1 =
126  let hcut = transrel_rect_Type3 h1 hterm in hcut __
127
128(** val transrel_inv_rect_Type2 :
129    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
130let transrel_inv_rect_Type2 hterm h1 =
131  let hcut = transrel_rect_Type2 h1 hterm in hcut __
132
133(** val transrel_inv_rect_Type1 :
134    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
135let transrel_inv_rect_Type1 hterm h1 =
136  let hcut = transrel_rect_Type1 h1 hterm in hcut __
137
138(** val transrel_inv_rect_Type0 :
139    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
140let transrel_inv_rect_Type0 hterm h1 =
141  let hcut = transrel_rect_Type0 h1 hterm in hcut __
142
143(** val transrel_jmdiscr : transrel -> transrel -> __ **)
144let transrel_jmdiscr x y =
145  Logic.eq_rect_Type2 x
146    (let Mk_transrel = x in Obj.magic (fun _ dH -> dH __ __ __)) y
147
148type program_behavior =
149| Terminates of Events.trace * Integers.int
150| Diverges of Events.trace
151| Reacts of Events.traceinf
152| Goes_wrong of Events.trace
153
154(** val program_behavior_rect_Type4 :
155    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
156    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
157    'a1 **)
158let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
159| Terminates (x_6965, x_6964) -> h_Terminates x_6965 x_6964
160| Diverges x_6966 -> h_Diverges x_6966
161| Reacts x_6967 -> h_Reacts x_6967
162| Goes_wrong x_6968 -> h_Goes_wrong x_6968
163
164(** val program_behavior_rect_Type5 :
165    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
166    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
167    'a1 **)
168let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
169| Terminates (x_6975, x_6974) -> h_Terminates x_6975 x_6974
170| Diverges x_6976 -> h_Diverges x_6976
171| Reacts x_6977 -> h_Reacts x_6977
172| Goes_wrong x_6978 -> h_Goes_wrong x_6978
173
174(** val program_behavior_rect_Type3 :
175    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
176    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
177    'a1 **)
178let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
179| Terminates (x_6985, x_6984) -> h_Terminates x_6985 x_6984
180| Diverges x_6986 -> h_Diverges x_6986
181| Reacts x_6987 -> h_Reacts x_6987
182| Goes_wrong x_6988 -> h_Goes_wrong x_6988
183
184(** val program_behavior_rect_Type2 :
185    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
186    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
187    'a1 **)
188let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
189| Terminates (x_6995, x_6994) -> h_Terminates x_6995 x_6994
190| Diverges x_6996 -> h_Diverges x_6996
191| Reacts x_6997 -> h_Reacts x_6997
192| Goes_wrong x_6998 -> h_Goes_wrong x_6998
193
194(** val program_behavior_rect_Type1 :
195    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
196    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
197    'a1 **)
198let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
199| Terminates (x_7005, x_7004) -> h_Terminates x_7005 x_7004
200| Diverges x_7006 -> h_Diverges x_7006
201| Reacts x_7007 -> h_Reacts x_7007
202| Goes_wrong x_7008 -> h_Goes_wrong x_7008
203
204(** val program_behavior_rect_Type0 :
205    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
206    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
207    'a1 **)
208let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
209| Terminates (x_7015, x_7014) -> h_Terminates x_7015 x_7014
210| Diverges x_7016 -> h_Diverges x_7016
211| Reacts x_7017 -> h_Reacts x_7017
212| Goes_wrong x_7018 -> h_Goes_wrong x_7018
213
214(** val program_behavior_inv_rect_Type4 :
215    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
216    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
217    (Events.trace -> __ -> 'a1) -> 'a1 **)
218let program_behavior_inv_rect_Type4 hterm h1 h2 h3 h4 =
219  let hcut = program_behavior_rect_Type4 h1 h2 h3 h4 hterm in hcut __
220
221(** val program_behavior_inv_rect_Type3 :
222    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
223    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
224    (Events.trace -> __ -> 'a1) -> 'a1 **)
225let program_behavior_inv_rect_Type3 hterm h1 h2 h3 h4 =
226  let hcut = program_behavior_rect_Type3 h1 h2 h3 h4 hterm in hcut __
227
228(** val program_behavior_inv_rect_Type2 :
229    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
230    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
231    (Events.trace -> __ -> 'a1) -> 'a1 **)
232let program_behavior_inv_rect_Type2 hterm h1 h2 h3 h4 =
233  let hcut = program_behavior_rect_Type2 h1 h2 h3 h4 hterm in hcut __
234
235(** val program_behavior_inv_rect_Type1 :
236    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
237    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
238    (Events.trace -> __ -> 'a1) -> 'a1 **)
239let program_behavior_inv_rect_Type1 hterm h1 h2 h3 h4 =
240  let hcut = program_behavior_rect_Type1 h1 h2 h3 h4 hterm in hcut __
241
242(** val program_behavior_inv_rect_Type0 :
243    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
244    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
245    (Events.trace -> __ -> 'a1) -> 'a1 **)
246let program_behavior_inv_rect_Type0 hterm h1 h2 h3 h4 =
247  let hcut = program_behavior_rect_Type0 h1 h2 h3 h4 hterm in hcut __
248
249(** val program_behavior_discr :
250    program_behavior -> program_behavior -> __ **)
251let program_behavior_discr x y =
252  Logic.eq_rect_Type2 x
253    (match x with
254     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
255     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
256     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
257     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
258
259(** val program_behavior_jmdiscr :
260    program_behavior -> program_behavior -> __ **)
261let program_behavior_jmdiscr x y =
262  Logic.eq_rect_Type2 x
263    (match x with
264     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
265     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
266     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
267     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
268
269type semantics = { trans : transrel; ge : __ }
270
271(** val semantics_rect_Type4 :
272    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
273let rec semantics_rect_Type4 h_mk_semantics x_7345 =
274  let { trans = trans0; ge = ge0 } = x_7345 in
275  h_mk_semantics trans0 __ __ ge0
276
277(** val semantics_rect_Type5 :
278    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
279let rec semantics_rect_Type5 h_mk_semantics x_7347 =
280  let { trans = trans0; ge = ge0 } = x_7347 in
281  h_mk_semantics trans0 __ __ ge0
282
283(** val semantics_rect_Type3 :
284    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
285let rec semantics_rect_Type3 h_mk_semantics x_7349 =
286  let { trans = trans0; ge = ge0 } = x_7349 in
287  h_mk_semantics trans0 __ __ ge0
288
289(** val semantics_rect_Type2 :
290    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
291let rec semantics_rect_Type2 h_mk_semantics x_7351 =
292  let { trans = trans0; ge = ge0 } = x_7351 in
293  h_mk_semantics trans0 __ __ ge0
294
295(** val semantics_rect_Type1 :
296    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
297let rec semantics_rect_Type1 h_mk_semantics x_7353 =
298  let { trans = trans0; ge = ge0 } = x_7353 in
299  h_mk_semantics trans0 __ __ ge0
300
301(** val semantics_rect_Type0 :
302    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
303let rec semantics_rect_Type0 h_mk_semantics x_7355 =
304  let { trans = trans0; ge = ge0 } = x_7355 in
305  h_mk_semantics trans0 __ __ ge0
306
307(** val trans : semantics -> transrel **)
308let rec trans xxx =
309  xxx.trans
310
311(** val ge : semantics -> __ **)
312let rec ge xxx =
313  xxx.ge
314
315(** val semantics_inv_rect_Type4 :
316    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
317let semantics_inv_rect_Type4 hterm h1 =
318  let hcut = semantics_rect_Type4 h1 hterm in hcut __
319
320(** val semantics_inv_rect_Type3 :
321    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
322let semantics_inv_rect_Type3 hterm h1 =
323  let hcut = semantics_rect_Type3 h1 hterm in hcut __
324
325(** val semantics_inv_rect_Type2 :
326    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
327let semantics_inv_rect_Type2 hterm h1 =
328  let hcut = semantics_rect_Type2 h1 hterm in hcut __
329
330(** val semantics_inv_rect_Type1 :
331    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
332let semantics_inv_rect_Type1 hterm h1 =
333  let hcut = semantics_rect_Type1 h1 hterm in hcut __
334
335(** val semantics_inv_rect_Type0 :
336    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
337let semantics_inv_rect_Type0 hterm h1 =
338  let hcut = semantics_rect_Type0 h1 hterm in hcut __
339
340(** val semantics_jmdiscr : semantics -> semantics -> __ **)
341let semantics_jmdiscr x y =
342  Logic.eq_rect_Type2 x
343    (let { trans = a0; ge = a3 } = x in
344    Obj.magic (fun _ dH -> dH __ __ __ __)) y
345
346type related_semantics = { sem1 : semantics; sem2 : semantics }
347
348(** val related_semantics_rect_Type4 :
349    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
350    'a1 **)
351let rec related_semantics_rect_Type4 h_mk_related_semantics x_7374 =
352  let { sem1 = sem3; sem2 = sem4 } = x_7374 in
353  h_mk_related_semantics sem3 sem4 __ __ __
354
355(** val related_semantics_rect_Type5 :
356    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
357    'a1 **)
358let rec related_semantics_rect_Type5 h_mk_related_semantics x_7376 =
359  let { sem1 = sem3; sem2 = sem4 } = x_7376 in
360  h_mk_related_semantics sem3 sem4 __ __ __
361
362(** val related_semantics_rect_Type3 :
363    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
364    'a1 **)
365let rec related_semantics_rect_Type3 h_mk_related_semantics x_7378 =
366  let { sem1 = sem3; sem2 = sem4 } = x_7378 in
367  h_mk_related_semantics sem3 sem4 __ __ __
368
369(** val related_semantics_rect_Type2 :
370    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
371    'a1 **)
372let rec related_semantics_rect_Type2 h_mk_related_semantics x_7380 =
373  let { sem1 = sem3; sem2 = sem4 } = x_7380 in
374  h_mk_related_semantics sem3 sem4 __ __ __
375
376(** val related_semantics_rect_Type1 :
377    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
378    'a1 **)
379let rec related_semantics_rect_Type1 h_mk_related_semantics x_7382 =
380  let { sem1 = sem3; sem2 = sem4 } = x_7382 in
381  h_mk_related_semantics sem3 sem4 __ __ __
382
383(** val related_semantics_rect_Type0 :
384    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
385    'a1 **)
386let rec related_semantics_rect_Type0 h_mk_related_semantics x_7384 =
387  let { sem1 = sem3; sem2 = sem4 } = x_7384 in
388  h_mk_related_semantics sem3 sem4 __ __ __
389
390(** val sem1 : related_semantics -> semantics **)
391let rec sem1 xxx =
392  xxx.sem1
393
394(** val sem2 : related_semantics -> semantics **)
395let rec sem2 xxx =
396  xxx.sem2
397
398(** val related_semantics_inv_rect_Type4 :
399    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
400    'a1) -> 'a1 **)
401let related_semantics_inv_rect_Type4 hterm h1 =
402  let hcut = related_semantics_rect_Type4 h1 hterm in hcut __
403
404(** val related_semantics_inv_rect_Type3 :
405    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
406    'a1) -> 'a1 **)
407let related_semantics_inv_rect_Type3 hterm h1 =
408  let hcut = related_semantics_rect_Type3 h1 hterm in hcut __
409
410(** val related_semantics_inv_rect_Type2 :
411    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
412    'a1) -> 'a1 **)
413let related_semantics_inv_rect_Type2 hterm h1 =
414  let hcut = related_semantics_rect_Type2 h1 hterm in hcut __
415
416(** val related_semantics_inv_rect_Type1 :
417    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
418    'a1) -> 'a1 **)
419let related_semantics_inv_rect_Type1 hterm h1 =
420  let hcut = related_semantics_rect_Type1 h1 hterm in hcut __
421
422(** val related_semantics_inv_rect_Type0 :
423    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
424    'a1) -> 'a1 **)
425let related_semantics_inv_rect_Type0 hterm h1 =
426  let hcut = related_semantics_rect_Type0 h1 hterm in hcut __
427
428(** val related_semantics_jmdiscr :
429    related_semantics -> related_semantics -> __ **)
430let related_semantics_jmdiscr x y =
431  Logic.eq_rect_Type2 x
432    (let { sem1 = a0; sem2 = a1 } = x in
433    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
434
435type order_sim =
436  related_semantics
437  (* singleton inductive, whose constructor was mk_order_sim *)
438
439(** val order_sim_rect_Type4 :
440    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
441let rec order_sim_rect_Type4 h_mk_order_sim x_7405 =
442  let sem = x_7405 in h_mk_order_sim sem __ __
443
444(** val order_sim_rect_Type5 :
445    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
446let rec order_sim_rect_Type5 h_mk_order_sim x_7407 =
447  let sem = x_7407 in h_mk_order_sim sem __ __
448
449(** val order_sim_rect_Type3 :
450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
451let rec order_sim_rect_Type3 h_mk_order_sim x_7409 =
452  let sem = x_7409 in h_mk_order_sim sem __ __
453
454(** val order_sim_rect_Type2 :
455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
456let rec order_sim_rect_Type2 h_mk_order_sim x_7411 =
457  let sem = x_7411 in h_mk_order_sim sem __ __
458
459(** val order_sim_rect_Type1 :
460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
461let rec order_sim_rect_Type1 h_mk_order_sim x_7413 =
462  let sem = x_7413 in h_mk_order_sim sem __ __
463
464(** val order_sim_rect_Type0 :
465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
466let rec order_sim_rect_Type0 h_mk_order_sim x_7415 =
467  let sem = x_7415 in h_mk_order_sim sem __ __
468
469(** val sem : order_sim -> related_semantics **)
470let rec sem xxx =
471  let yyy = xxx in yyy
472
473(** val order_sim_inv_rect_Type4 :
474    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
475let order_sim_inv_rect_Type4 hterm h1 =
476  let hcut = order_sim_rect_Type4 h1 hterm in hcut __
477
478(** val order_sim_inv_rect_Type3 :
479    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
480let order_sim_inv_rect_Type3 hterm h1 =
481  let hcut = order_sim_rect_Type3 h1 hterm in hcut __
482
483(** val order_sim_inv_rect_Type2 :
484    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
485let order_sim_inv_rect_Type2 hterm h1 =
486  let hcut = order_sim_rect_Type2 h1 hterm in hcut __
487
488(** val order_sim_inv_rect_Type1 :
489    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
490let order_sim_inv_rect_Type1 hterm h1 =
491  let hcut = order_sim_rect_Type1 h1 hterm in hcut __
492
493(** val order_sim_inv_rect_Type0 :
494    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
495let order_sim_inv_rect_Type0 hterm h1 =
496  let hcut = order_sim_rect_Type0 h1 hterm in hcut __
497
498(** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
499let order_sim_jmdiscr x y =
500  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
501
Note: See TracBrowser for help on using the repository browser.