source: extracted/simplifyCasts.mli @ 2649

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

...

File size: 4.0 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open TypeComparison
76
77open ClassifyOp
78
79open Smallstep
80
81open Extra_bool
82
83open FrontEndVal
84
85open Hide
86
87open ByteValues
88
89open GenMem
90
91open FrontEndMem
92
93open Globalenvs
94
95open Csem
96
97open SmallstepExec
98
99open Division
100
101open Z
102
103open BitVectorZ
104
105open Pointers
106
107open Values
108
109open Events
110
111open IOMonad
112
113open IO
114
115open Cexec
116
117open Casts
118
119open CexecInd
120
121open CexecSound
122
123open Sets
124
125open Listb
126
127open Star
128
129open Frontend_misc
130
131val reduce_bits :
132  Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
133  BitVector.bitVector Types.option
134
135val pred_bitsize_of_intsize : AST.intsize -> Nat.nat
136
137val signed : AST.signedness -> Bool.bool
138
139val simplify_int :
140  AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> AST.bvint
141  -> AST.bvint Types.option
142
143val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum
144
145val size_not_lt_to_ge : AST.intsize -> AST.intsize -> (__, __) Types.sum
146
147val sign_eq_dect : AST.signedness -> AST.signedness -> (__, __) Types.sum
148
149val necessary_conditions :
150  AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> Bool.bool
151
152val assert_int_value :
153  Values.val0 Types.option -> AST.intsize -> BitVector.bitVector Types.option
154
155val binop_simplifiable : Csyntax.binary_operation -> Bool.bool
156
157val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0
158
159val simplify_expr :
160  Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, Csyntax.expr)
161  Types.prod Types.sig0
162
163val simplify_e : Csyntax.expr -> Csyntax.expr
164
165val simplify_ls : Csyntax.labeled_statements -> Csyntax.labeled_statements
166
167val simplify_statement : Csyntax.statement -> Csyntax.statement
168
169val simplify_function : Csyntax.function0 -> Csyntax.function0
170
171val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef
172
173val simplify_program : Csyntax.clight_program -> Csyntax.clight_program
174
175val related_globals_rect_Type6 :
176  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
177  -> __ -> 'a2) -> 'a2
178
179val related_globals_rect_Type7 :
180  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
181  -> __ -> 'a2) -> 'a2
182
183val related_globals_rect_Type8 :
184  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
185  -> __ -> 'a2) -> 'a2
186
187val related_globals_rect_Type9 :
188  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
189  -> __ -> 'a2) -> 'a2
190
191val related_globals_rect_Type10 :
192  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
193  -> __ -> 'a2) -> 'a2
194
195val related_globals_rect_Type11 :
196  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
197  -> __ -> 'a2) -> 'a2
198
199val related_globals_inv_rect_Type5 :
200  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
201  -> __ -> __ -> 'a2) -> 'a2
202
203val related_globals_inv_rect_Type6 :
204  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
205  -> __ -> __ -> 'a2) -> 'a2
206
207val related_globals_inv_rect_Type7 :
208  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
209  -> __ -> __ -> 'a2) -> 'a2
210
211val related_globals_inv_rect_Type8 :
212  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
213  -> __ -> __ -> 'a2) -> 'a2
214
215val related_globals_inv_rect_Type9 :
216  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
217  -> __ -> __ -> 'a2) -> 'a2
218
219val related_globals_discr0 :
220  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
221
222val related_globals_jmdiscr0 :
223  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
224
Note: See TracBrowser for help on using the repository browser.