source: extracted/simplifyCasts.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: 4.0 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 TypeComparison
80
81open ClassifyOp
82
83open Smallstep
84
85open Extra_bool
86
87open FrontEndVal
88
89open Hide
90
91open ByteValues
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
99open Csem
100
101open SmallstepExec
102
103open Division
104
105open Z
106
107open BitVectorZ
108
109open Pointers
110
111open Values
112
113open Events
114
115open IOMonad
116
117open IO
118
119open Cexec
120
121open Casts
122
123open CexecInd
124
125open CexecSound
126
127open Sets
128
129open Listb
130
131open Star
132
133open Frontend_misc
134
135val reduce_bits :
136  Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
137  BitVector.bitVector Types.option
138
139val pred_bitsize_of_intsize : AST.intsize -> Nat.nat
140
141val signed : AST.signedness -> Bool.bool
142
143val simplify_int :
144  AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> AST.bvint
145  -> AST.bvint Types.option
146
147val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum
148
149val size_not_lt_to_ge : AST.intsize -> AST.intsize -> (__, __) Types.sum
150
151val sign_eq_dect : AST.signedness -> AST.signedness -> (__, __) Types.sum
152
153val necessary_conditions :
154  AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> Bool.bool
155
156val assert_int_value :
157  Values.val0 Types.option -> AST.intsize -> BitVector.bitVector Types.option
158
159val binop_simplifiable : Csyntax.binary_operation -> Bool.bool
160
161val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0
162
163val simplify_expr :
164  Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, Csyntax.expr)
165  Types.prod Types.sig0
166
167val simplify_e : Csyntax.expr -> Csyntax.expr
168
169val simplify_ls : Csyntax.labeled_statements -> Csyntax.labeled_statements
170
171val simplify_statement : Csyntax.statement -> Csyntax.statement
172
173val simplify_function : Csyntax.function0 -> Csyntax.function0
174
175val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef
176
177val simplify_program : Csyntax.clight_program -> Csyntax.clight_program
178
179val related_globals_rect_Type6 :
180  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
181  -> __ -> 'a2) -> 'a2
182
183val related_globals_rect_Type7 :
184  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
185  -> __ -> 'a2) -> 'a2
186
187val related_globals_rect_Type8 :
188  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
189  -> __ -> 'a2) -> 'a2
190
191val related_globals_rect_Type9 :
192  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
193  -> __ -> 'a2) -> 'a2
194
195val related_globals_rect_Type10 :
196  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
197  -> __ -> 'a2) -> 'a2
198
199val related_globals_rect_Type11 :
200  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
201  -> __ -> 'a2) -> 'a2
202
203val related_globals_inv_rect_Type5 :
204  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
205  -> __ -> __ -> 'a2) -> 'a2
206
207val related_globals_inv_rect_Type6 :
208  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
209  -> __ -> __ -> 'a2) -> 'a2
210
211val related_globals_inv_rect_Type7 :
212  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
213  -> __ -> __ -> 'a2) -> 'a2
214
215val related_globals_inv_rect_Type8 :
216  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
217  -> __ -> __ -> 'a2) -> 'a2
218
219val related_globals_inv_rect_Type9 :
220  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
221  -> __ -> __ -> 'a2) -> 'a2
222
223val related_globals_discr0 :
224  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
225
226val related_globals_jmdiscr0 :
227  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
228
Note: See TracBrowser for help on using the repository browser.