source: extracted/switchRemoval.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 7.5 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Coqlib
30
31open Floats
32
33open Arithmetic
34
35open Char
36
37open String
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open Fresh
80
81open TypeComparison
82
83open ClassifyOp
84
85open Smallstep
86
87open Extra_bool
88
89open FrontEndVal
90
91open Hide
92
93open ByteValues
94
95open GenMem
96
97open FrontEndMem
98
99open Globalenvs
100
101open Csem
102
103open SmallstepExec
104
105open Division
106
107open Z
108
109open BitVectorZ
110
111open Pointers
112
113open Values
114
115open Events
116
117open IOMonad
118
119open IO
120
121open Cexec
122
123open CexecInd
124
125open Sets
126
127open Listb
128
129open Star
130
131open Frontend_misc
132
133open MemProperties
134
135open MemoryInjections
136
137type switch_free = __
138
139type branches_switch_free = __
140
141val convert_break_to_goto :
142  Csyntax.statement -> Csyntax.label -> Csyntax.statement
143
144val produce_cond :
145  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
146  Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
147  Identifiers.universe) Types.prod
148
149val simplify_switch :
150  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
151  (Csyntax.statement, Identifiers.universe) Types.prod
152
153val switch_removal_branches :
154  Csyntax.labeled_statements -> Identifiers.universe ->
155  ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
156  List.list) Types.prod, Identifiers.universe) Types.prod
157
158val switch_removal :
159  Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
160  (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
161  Identifiers.universe) Types.prod
162
163val ret_st :
164  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
165  Identifiers.universe) Types.prod -> 'a1
166
167val ret_vars :
168  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
169  Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
170  List.list
171
172val ret_u :
173  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
174  Identifiers.universe) Types.prod -> Identifiers.universe
175
176val least_identifier : PreIdentifiers.identifier
177
178val max_of_expr : Csyntax.expr -> AST.ident
179
180val max_of_ls : Csyntax.labeled_statements -> AST.ident
181
182val max_of_statement : Csyntax.statement -> AST.ident
183
184val max_id_of_function : Csyntax.function0 -> AST.ident
185
186val function_switch_removal :
187  Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
188  Types.prod List.list) Types.prod
189
190val fundef_switch_removal : Csyntax.clight_fundef -> Csyntax.clight_fundef
191
192val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program
193
194type substatement_ls = __
195
196type substatement_P = __
197
198val nonempty_block_rect_Type4 :
199  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
200
201val nonempty_block_rect_Type5 :
202  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
203
204val nonempty_block_rect_Type3 :
205  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
206
207val nonempty_block_rect_Type2 :
208  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
209
210val nonempty_block_rect_Type1 :
211  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
212
213val nonempty_block_rect_Type0 :
214  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
215
216val nonempty_block_inv_rect_Type4 :
217  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
218
219val nonempty_block_inv_rect_Type3 :
220  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
221
222val nonempty_block_inv_rect_Type2 :
223  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
224
225val nonempty_block_inv_rect_Type1 :
226  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
227
228val nonempty_block_inv_rect_Type0 :
229  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
230
231val nonempty_block_discr : GenMem.mem1 -> Pointers.block -> __
232
233val nonempty_block_jmdiscr : GenMem.mem1 -> Pointers.block -> __
234
235val sr_memext_rect_Type4 :
236  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
237  -> 'a1) -> 'a1
238
239val sr_memext_rect_Type5 :
240  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
241  -> 'a1) -> 'a1
242
243val sr_memext_rect_Type3 :
244  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
245  -> 'a1) -> 'a1
246
247val sr_memext_rect_Type2 :
248  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
249  -> 'a1) -> 'a1
250
251val sr_memext_rect_Type1 :
252  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
253  -> 'a1) -> 'a1
254
255val sr_memext_rect_Type0 :
256  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
257  -> 'a1) -> 'a1
258
259val sr_memext_inv_rect_Type4 :
260  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
261  -> __ -> 'a1) -> 'a1
262
263val sr_memext_inv_rect_Type3 :
264  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
265  -> __ -> 'a1) -> 'a1
266
267val sr_memext_inv_rect_Type2 :
268  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
269  -> __ -> 'a1) -> 'a1
270
271val sr_memext_inv_rect_Type1 :
272  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
273  -> __ -> 'a1) -> 'a1
274
275val sr_memext_inv_rect_Type0 :
276  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
277  -> __ -> 'a1) -> 'a1
278
279val sr_memext_discr :
280  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
281
282val sr_memext_jmdiscr :
283  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
284
285val env_codomain :
286  Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
287  Pointers.block Frontend_misc.lset
288
289val switch_removal_globals_rect_Type4 :
290  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
291  -> __ -> 'a2) -> 'a2
292
293val switch_removal_globals_rect_Type5 :
294  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
295  -> __ -> 'a2) -> 'a2
296
297val switch_removal_globals_rect_Type3 :
298  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
299  -> __ -> 'a2) -> 'a2
300
301val switch_removal_globals_rect_Type2 :
302  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
303  -> __ -> 'a2) -> 'a2
304
305val switch_removal_globals_rect_Type1 :
306  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
307  -> __ -> 'a2) -> 'a2
308
309val switch_removal_globals_rect_Type0 :
310  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
311  -> __ -> 'a2) -> 'a2
312
313val switch_removal_globals_inv_rect_Type4 :
314  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
315  -> __ -> __ -> 'a2) -> 'a2
316
317val switch_removal_globals_inv_rect_Type3 :
318  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
319  -> __ -> __ -> 'a2) -> 'a2
320
321val switch_removal_globals_inv_rect_Type2 :
322  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
323  -> __ -> __ -> 'a2) -> 'a2
324
325val switch_removal_globals_inv_rect_Type1 :
326  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
327  -> __ -> __ -> 'a2) -> 'a2
328
329val switch_removal_globals_inv_rect_Type0 :
330  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
331  -> __ -> __ -> 'a2) -> 'a2
332
333val switch_removal_globals_discr :
334  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
335
336val switch_removal_globals_jmdiscr :
337  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
338
Note: See TracBrowser for help on using the repository browser.