source: driver/extracted/events.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: 11.1 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
21open Exp
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open CostLabel
84
85type eventval =
86| EVint of AST.intsize * AST.bvint
87
88(** val eventval_rect_Type4 :
89    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
90let rec eventval_rect_Type4 h_EVint = function
91| EVint (sz, x_5537) -> h_EVint sz x_5537
92
93(** val eventval_rect_Type5 :
94    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
95let rec eventval_rect_Type5 h_EVint = function
96| EVint (sz, x_5540) -> h_EVint sz x_5540
97
98(** val eventval_rect_Type3 :
99    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
100let rec eventval_rect_Type3 h_EVint = function
101| EVint (sz, x_5543) -> h_EVint sz x_5543
102
103(** val eventval_rect_Type2 :
104    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
105let rec eventval_rect_Type2 h_EVint = function
106| EVint (sz, x_5546) -> h_EVint sz x_5546
107
108(** val eventval_rect_Type1 :
109    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
110let rec eventval_rect_Type1 h_EVint = function
111| EVint (sz, x_5549) -> h_EVint sz x_5549
112
113(** val eventval_rect_Type0 :
114    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
115let rec eventval_rect_Type0 h_EVint = function
116| EVint (sz, x_5552) -> h_EVint sz x_5552
117
118(** val eventval_inv_rect_Type4 :
119    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
120let eventval_inv_rect_Type4 hterm h1 =
121  let hcut = eventval_rect_Type4 h1 hterm in hcut __
122
123(** val eventval_inv_rect_Type3 :
124    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
125let eventval_inv_rect_Type3 hterm h1 =
126  let hcut = eventval_rect_Type3 h1 hterm in hcut __
127
128(** val eventval_inv_rect_Type2 :
129    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
130let eventval_inv_rect_Type2 hterm h1 =
131  let hcut = eventval_rect_Type2 h1 hterm in hcut __
132
133(** val eventval_inv_rect_Type1 :
134    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
135let eventval_inv_rect_Type1 hterm h1 =
136  let hcut = eventval_rect_Type1 h1 hterm in hcut __
137
138(** val eventval_inv_rect_Type0 :
139    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
140let eventval_inv_rect_Type0 hterm h1 =
141  let hcut = eventval_rect_Type0 h1 hterm in hcut __
142
143(** val eventval_discr : eventval -> eventval -> __ **)
144let eventval_discr x y =
145  Logic.eq_rect_Type2 x
146    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
147
148(** val eventval_jmdiscr : eventval -> eventval -> __ **)
149let eventval_jmdiscr x y =
150  Logic.eq_rect_Type2 x
151    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
152
153type event =
154| EVcost of CostLabel.costlabel
155| EVextcall of AST.ident * eventval List.list * eventval
156
157(** val event_rect_Type4 :
158    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
159    eventval -> 'a1) -> event -> 'a1 **)
160let rec event_rect_Type4 h_EVcost h_EVextcall = function
161| EVcost x_5577 -> h_EVcost x_5577
162| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
163
164(** val event_rect_Type5 :
165    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
166    eventval -> 'a1) -> event -> 'a1 **)
167let rec event_rect_Type5 h_EVcost h_EVextcall = function
168| EVcost x_5581 -> h_EVcost x_5581
169| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
170
171(** val event_rect_Type3 :
172    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
173    eventval -> 'a1) -> event -> 'a1 **)
174let rec event_rect_Type3 h_EVcost h_EVextcall = function
175| EVcost x_5585 -> h_EVcost x_5585
176| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
177
178(** val event_rect_Type2 :
179    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
180    eventval -> 'a1) -> event -> 'a1 **)
181let rec event_rect_Type2 h_EVcost h_EVextcall = function
182| EVcost x_5589 -> h_EVcost x_5589
183| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
184
185(** val event_rect_Type1 :
186    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
187    eventval -> 'a1) -> event -> 'a1 **)
188let rec event_rect_Type1 h_EVcost h_EVextcall = function
189| EVcost x_5593 -> h_EVcost x_5593
190| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
191
192(** val event_rect_Type0 :
193    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
194    eventval -> 'a1) -> event -> 'a1 **)
195let rec event_rect_Type0 h_EVcost h_EVextcall = function
196| EVcost x_5597 -> h_EVcost x_5597
197| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
198
199(** val event_inv_rect_Type4 :
200    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
201    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
202let event_inv_rect_Type4 hterm h1 h2 =
203  let hcut = event_rect_Type4 h1 h2 hterm in hcut __
204
205(** val event_inv_rect_Type3 :
206    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
207    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
208let event_inv_rect_Type3 hterm h1 h2 =
209  let hcut = event_rect_Type3 h1 h2 hterm in hcut __
210
211(** val event_inv_rect_Type2 :
212    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
213    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
214let event_inv_rect_Type2 hterm h1 h2 =
215  let hcut = event_rect_Type2 h1 h2 hterm in hcut __
216
217(** val event_inv_rect_Type1 :
218    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
219    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
220let event_inv_rect_Type1 hterm h1 h2 =
221  let hcut = event_rect_Type1 h1 h2 hterm in hcut __
222
223(** val event_inv_rect_Type0 :
224    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
225    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
226let event_inv_rect_Type0 hterm h1 h2 =
227  let hcut = event_rect_Type0 h1 h2 hterm in hcut __
228
229(** val event_discr : event -> event -> __ **)
230let event_discr x y =
231  Logic.eq_rect_Type2 x
232    (match x with
233     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
234     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
235
236(** val event_jmdiscr : event -> event -> __ **)
237let event_jmdiscr x y =
238  Logic.eq_rect_Type2 x
239    (match x with
240     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
241     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
242
243type trace = event List.list
244
245(** val e0 : trace **)
246let e0 =
247  List.Nil
248
249(** val echarge : CostLabel.costlabel -> trace **)
250let echarge label =
251  List.Cons ((EVcost label), List.Nil)
252
253(** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
254let eextcall name args res =
255  List.Cons ((EVextcall (name, args, res)), List.Nil)
256
257(** val eapp : trace -> trace -> trace **)
258let eapp t1 t2 =
259  List.append t1 t2
260
261type traceinf = __traceinf Lazy.t
262and __traceinf =
263| Econsinf of event * traceinf
264
265(** val traceinf_inv_rect_Type4 :
266    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
267let traceinf_inv_rect_Type4 hterm h1 =
268  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
269
270(** val traceinf_inv_rect_Type3 :
271    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
272let traceinf_inv_rect_Type3 hterm h1 =
273  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
274
275(** val traceinf_inv_rect_Type2 :
276    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
277let traceinf_inv_rect_Type2 hterm h1 =
278  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
279
280(** val traceinf_inv_rect_Type1 :
281    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
282let traceinf_inv_rect_Type1 hterm h1 =
283  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
284
285(** val traceinf_inv_rect_Type0 :
286    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
287let traceinf_inv_rect_Type0 hterm h1 =
288  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
289
290(** val traceinf_discr : traceinf -> traceinf -> __ **)
291let traceinf_discr x y =
292  Logic.eq_rect_Type2 x
293    (let Econsinf (a0, a1) = Lazy.force x in
294    Obj.magic (fun _ dH -> dH __ __)) y
295
296(** val traceinf_jmdiscr : traceinf -> traceinf -> __ **)
297let traceinf_jmdiscr x y =
298  Logic.eq_rect_Type2 x
299    (let Econsinf (a0, a1) = Lazy.force x in
300    Obj.magic (fun _ dH -> dH __ __)) y
301
302(** val eappinf : trace -> traceinf -> traceinf **)
303let rec eappinf t t0 =
304  match t with
305  | List.Nil -> t0
306  | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0)))
307
308(** val remove_costs : trace -> trace **)
309let remove_costs =
310  List.filter (fun e ->
311    match e with
312    | EVcost x -> Bool.False
313    | EVextcall (x, x0, x1) -> Bool.True)
314
315type traceinf' = __traceinf' Lazy.t
316and __traceinf' =
317| Econsinf' of trace * traceinf'
318
319(** val traceinf'_inv_rect_Type4 :
320    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
321let traceinf'_inv_rect_Type4 hterm h1 =
322  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
323  hcut __
324
325(** val traceinf'_inv_rect_Type3 :
326    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
327let traceinf'_inv_rect_Type3 hterm h1 =
328  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
329  hcut __
330
331(** val traceinf'_inv_rect_Type2 :
332    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
333let traceinf'_inv_rect_Type2 hterm h1 =
334  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
335  hcut __
336
337(** val traceinf'_inv_rect_Type1 :
338    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
339let traceinf'_inv_rect_Type1 hterm h1 =
340  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
341  hcut __
342
343(** val traceinf'_inv_rect_Type0 :
344    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
345let traceinf'_inv_rect_Type0 hterm h1 =
346  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
347  hcut __
348
349(** val traceinf'_discr : traceinf' -> traceinf' -> __ **)
350let traceinf'_discr x y =
351  Logic.eq_rect_Type2 x
352    (let Econsinf' (a0, a1) = Lazy.force x in
353    Obj.magic (fun _ dH -> dH __ __ __)) y
354
355(** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **)
356let traceinf'_jmdiscr x y =
357  Logic.eq_rect_Type2 x
358    (let Econsinf' (a0, a1) = Lazy.force x in
359    Obj.magic (fun _ dH -> dH __ __ __)) y
360
361(** val split_traceinf' :
362    trace -> traceinf' -> (event, traceinf') Types.prod **)
363let split_traceinf' t t0 =
364  (match t with
365   | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
366   | List.Cons (e, t') ->
367     (fun _ ->
368       (match t' with
369        | List.Nil -> (fun _ -> { Types.fst = e; Types.snd = t0 })
370        | List.Cons (e', t'') ->
371          (fun _ -> { Types.fst = e; Types.snd = (lazy (Econsinf' (t',
372            t0))) })) __)) __
373
374(** val traceinf_of_traceinf' : traceinf' -> traceinf **)
375let rec traceinf_of_traceinf' t' =
376  let Econsinf' (t, t'') = Lazy.force t' in
377  let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in
378  lazy (Econsinf (e, (traceinf_of_traceinf' tl)))
379
Note: See TracBrowser for help on using the repository browser.