69 open Hints_declaration
94 | Ointconst of AST.intsize * AST.signedness * AST.bvint
95 | Oaddrsymbol of AST.ident * Nat.nat
96 | Oaddrstack of Nat.nat
98 (** val constant_rect_Type4 :
99 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
100 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
101 let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13118 = function
102 | Ointconst (sz, sg, x_13120) -> h_Ointconst sz sg x_13120
103 | Oaddrsymbol (x_13122, x_13121) -> h_Oaddrsymbol x_13122 x_13121
104 | Oaddrstack x_13123 -> h_Oaddrstack x_13123
106 (** val constant_rect_Type5 :
107 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
108 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
109 let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13127 = function
110 | Ointconst (sz, sg, x_13129) -> h_Ointconst sz sg x_13129
111 | Oaddrsymbol (x_13131, x_13130) -> h_Oaddrsymbol x_13131 x_13130
112 | Oaddrstack x_13132 -> h_Oaddrstack x_13132
114 (** val constant_rect_Type3 :
115 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
116 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
117 let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13136 = function
118 | Ointconst (sz, sg, x_13138) -> h_Ointconst sz sg x_13138
119 | Oaddrsymbol (x_13140, x_13139) -> h_Oaddrsymbol x_13140 x_13139
120 | Oaddrstack x_13141 -> h_Oaddrstack x_13141
122 (** val constant_rect_Type2 :
123 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
124 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
125 let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13145 = function
126 | Ointconst (sz, sg, x_13147) -> h_Ointconst sz sg x_13147
127 | Oaddrsymbol (x_13149, x_13148) -> h_Oaddrsymbol x_13149 x_13148
128 | Oaddrstack x_13150 -> h_Oaddrstack x_13150
130 (** val constant_rect_Type1 :
131 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
132 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
133 let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13154 = function
134 | Ointconst (sz, sg, x_13156) -> h_Ointconst sz sg x_13156
135 | Oaddrsymbol (x_13158, x_13157) -> h_Oaddrsymbol x_13158 x_13157
136 | Oaddrstack x_13159 -> h_Oaddrstack x_13159
138 (** val constant_rect_Type0 :
139 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
140 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
141 let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13163 = function
142 | Ointconst (sz, sg, x_13165) -> h_Ointconst sz sg x_13165
143 | Oaddrsymbol (x_13167, x_13166) -> h_Oaddrsymbol x_13167 x_13166
144 | Oaddrstack x_13168 -> h_Oaddrstack x_13168
146 (** val constant_inv_rect_Type4 :
147 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
148 -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
149 __ -> __ -> 'a1) -> 'a1 **)
150 let constant_inv_rect_Type4 x1 hterm h1 h2 h3 =
151 let hcut = constant_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
153 (** val constant_inv_rect_Type3 :
154 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
155 -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
156 __ -> __ -> 'a1) -> 'a1 **)
157 let constant_inv_rect_Type3 x1 hterm h1 h2 h3 =
158 let hcut = constant_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
160 (** val constant_inv_rect_Type2 :
161 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
162 -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
163 __ -> __ -> 'a1) -> 'a1 **)
164 let constant_inv_rect_Type2 x1 hterm h1 h2 h3 =
165 let hcut = constant_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
167 (** val constant_inv_rect_Type1 :
168 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
169 -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
170 __ -> __ -> 'a1) -> 'a1 **)
171 let constant_inv_rect_Type1 x1 hterm h1 h2 h3 =
172 let hcut = constant_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
174 (** val constant_inv_rect_Type0 :
175 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
176 -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
177 __ -> __ -> 'a1) -> 'a1 **)
178 let constant_inv_rect_Type0 x1 hterm h1 h2 h3 =
179 let hcut = constant_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
181 (** val constant_discr : AST.typ -> constant -> constant -> __ **)
182 let constant_discr a1 x y =
183 Logic.eq_rect_Type2 x
185 | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
186 | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
187 | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y
189 (** val constant_jmdiscr : AST.typ -> constant -> constant -> __ **)
190 let constant_jmdiscr a1 x y =
191 Logic.eq_rect_Type2 x
193 | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
194 | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
195 | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y
197 type unary_operation =
198 | Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
199 | Onegint of AST.intsize * AST.signedness
200 | Onotbool of AST.typ * AST.intsize * AST.signedness
201 | Onotint of AST.intsize * AST.signedness
203 | Optrofint of AST.intsize * AST.signedness
204 | Ointofptr of AST.intsize * AST.signedness
206 (** val unary_operation_rect_Type4 :
207 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
208 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
209 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
210 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
211 (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
212 unary_operation -> 'a1 **)
213 let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13238 x_13237 = function
214 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
215 | Onegint (sz, sg) -> h_Onegint sz sg
216 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
217 | Onotint (sz, sg) -> h_Onotint sz sg
219 | Optrofint (sz, sg) -> h_Optrofint sz sg
220 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
222 (** val unary_operation_rect_Type5 :
223 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
224 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
225 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
226 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
227 (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
228 unary_operation -> 'a1 **)
229 let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13249 x_13248 = function
230 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
231 | Onegint (sz, sg) -> h_Onegint sz sg
232 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
233 | Onotint (sz, sg) -> h_Onotint sz sg
235 | Optrofint (sz, sg) -> h_Optrofint sz sg
236 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
238 (** val unary_operation_rect_Type3 :
239 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
240 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
241 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
242 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
243 (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
244 unary_operation -> 'a1 **)
245 let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13260 x_13259 = function
246 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
247 | Onegint (sz, sg) -> h_Onegint sz sg
248 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
249 | Onotint (sz, sg) -> h_Onotint sz sg
251 | Optrofint (sz, sg) -> h_Optrofint sz sg
252 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
254 (** val unary_operation_rect_Type2 :
255 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
256 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
257 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
258 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
259 (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
260 unary_operation -> 'a1 **)
261 let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13271 x_13270 = function
262 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
263 | Onegint (sz, sg) -> h_Onegint sz sg
264 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
265 | Onotint (sz, sg) -> h_Onotint sz sg
267 | Optrofint (sz, sg) -> h_Optrofint sz sg
268 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
270 (** val unary_operation_rect_Type1 :
271 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
272 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
273 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
274 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
275 (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
276 unary_operation -> 'a1 **)
277 let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13282 x_13281 = function
278 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
279 | Onegint (sz, sg) -> h_Onegint sz sg
280 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
281 | Onotint (sz, sg) -> h_Onotint sz sg
283 | Optrofint (sz, sg) -> h_Optrofint sz sg
284 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
286 (** val unary_operation_rect_Type0 :
287 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
288 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
289 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
290 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
291 (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
292 unary_operation -> 'a1 **)
293 let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13293 x_13292 = function
294 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
295 | Onegint (sz, sg) -> h_Onegint sz sg
296 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
297 | Onotint (sz, sg) -> h_Onotint sz sg
299 | Optrofint (sz, sg) -> h_Optrofint sz sg
300 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
302 (** val unary_operation_inv_rect_Type4 :
303 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
304 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
305 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
306 AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
307 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
308 __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
309 __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
311 let unary_operation_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
312 let hcut = unary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
315 (** val unary_operation_inv_rect_Type3 :
316 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
317 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
318 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
319 AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
320 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
321 __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
322 __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
324 let unary_operation_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
325 let hcut = unary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
328 (** val unary_operation_inv_rect_Type2 :
329 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
330 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
331 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
332 AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
333 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
334 __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
335 __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
337 let unary_operation_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
338 let hcut = unary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
341 (** val unary_operation_inv_rect_Type1 :
342 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
343 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
344 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
345 AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
346 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
347 __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
348 __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
350 let unary_operation_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
351 let hcut = unary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
354 (** val unary_operation_inv_rect_Type0 :
355 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
356 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
357 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
358 AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
359 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
360 __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
361 __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
363 let unary_operation_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
364 let hcut = unary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
367 (** val unary_operation_discr :
368 AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
369 let unary_operation_discr a1 a2 x y =
370 Logic.eq_rect_Type2 x
372 | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
373 | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
374 | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
375 | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
376 | Oid a0 -> Obj.magic (fun _ dH -> dH __)
377 | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
378 | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
380 (** val unary_operation_jmdiscr :
381 AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
382 let unary_operation_jmdiscr a1 a2 x y =
383 Logic.eq_rect_Type2 x
385 | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
386 | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
387 | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
388 | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
389 | Oid a0 -> Obj.magic (fun _ dH -> dH __)
390 | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
391 | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
393 type binary_operation =
394 | Oadd of AST.intsize * AST.signedness
395 | Osub of AST.intsize * AST.signedness
396 | Omul of AST.intsize * AST.signedness
397 | Odiv of AST.intsize
398 | Odivu of AST.intsize
399 | Omod of AST.intsize
400 | Omodu of AST.intsize
401 | Oand of AST.intsize * AST.signedness
402 | Oor of AST.intsize * AST.signedness
403 | Oxor of AST.intsize * AST.signedness
404 | Oshl of AST.intsize * AST.signedness
405 | Oshr of AST.intsize * AST.signedness
406 | Oshru of AST.intsize * AST.signedness
407 | Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
408 | Ocmpu of AST.intsize * AST.signedness * Integers.comparison
409 | Oaddpi of AST.intsize
410 | Oaddip of AST.intsize
411 | Osubpi of AST.intsize
412 | Osubpp of AST.intsize
413 | Ocmpp of AST.signedness * Integers.comparison
415 (** val binary_operation_rect_Type4 :
416 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
417 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
418 -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
419 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
420 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
421 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
422 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
423 AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
424 (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
425 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
426 (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
427 AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
428 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13398 x_13397 x_13396 = function
429 | Oadd (sz, sg) -> h_Oadd sz sg
430 | Osub (sz, sg) -> h_Osub sz sg
431 | Omul (sz, sg) -> h_Omul sz sg
432 | Odiv sz -> h_Odiv sz
433 | Odivu sz -> h_Odivu sz
434 | Omod sz -> h_Omod sz
435 | Omodu sz -> h_Omodu sz
436 | Oand (sz, sg) -> h_Oand sz sg
437 | Oor (sz, sg) -> h_Oor sz sg
438 | Oxor (sz, sg) -> h_Oxor sz sg
439 | Oshl (sz, sg) -> h_Oshl sz sg
440 | Oshr (sz, sg) -> h_Oshr sz sg
441 | Oshru (sz, sg) -> h_Oshru sz sg
442 | Ocmp (sz, sg, sg', x_13400) -> h_Ocmp sz sg sg' x_13400
443 | Ocmpu (sz, sg', x_13401) -> h_Ocmpu sz sg' x_13401
444 | Oaddpi sz -> h_Oaddpi sz
445 | Oaddip sz -> h_Oaddip sz
446 | Osubpi sz -> h_Osubpi sz
447 | Osubpp sz -> h_Osubpp sz
448 | Ocmpp (sg', x_13402) -> h_Ocmpp sg' x_13402
450 (** val binary_operation_rect_Type5 :
451 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
452 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
453 -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
454 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
455 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
456 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
457 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
458 AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
459 (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
460 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
461 (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
462 AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
463 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13425 x_13424 x_13423 = function
464 | Oadd (sz, sg) -> h_Oadd sz sg
465 | Osub (sz, sg) -> h_Osub sz sg
466 | Omul (sz, sg) -> h_Omul sz sg
467 | Odiv sz -> h_Odiv sz
468 | Odivu sz -> h_Odivu sz
469 | Omod sz -> h_Omod sz
470 | Omodu sz -> h_Omodu sz
471 | Oand (sz, sg) -> h_Oand sz sg
472 | Oor (sz, sg) -> h_Oor sz sg
473 | Oxor (sz, sg) -> h_Oxor sz sg
474 | Oshl (sz, sg) -> h_Oshl sz sg
475 | Oshr (sz, sg) -> h_Oshr sz sg
476 | Oshru (sz, sg) -> h_Oshru sz sg
477 | Ocmp (sz, sg, sg', x_13427) -> h_Ocmp sz sg sg' x_13427
478 | Ocmpu (sz, sg', x_13428) -> h_Ocmpu sz sg' x_13428
479 | Oaddpi sz -> h_Oaddpi sz
480 | Oaddip sz -> h_Oaddip sz
481 | Osubpi sz -> h_Osubpi sz
482 | Osubpp sz -> h_Osubpp sz
483 | Ocmpp (sg', x_13429) -> h_Ocmpp sg' x_13429
485 (** val binary_operation_rect_Type3 :
486 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
487 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
488 -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
489 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
490 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
491 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
492 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
493 AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
494 (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
495 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
496 (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
497 AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
498 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13452 x_13451 x_13450 = function
499 | Oadd (sz, sg) -> h_Oadd sz sg
500 | Osub (sz, sg) -> h_Osub sz sg
501 | Omul (sz, sg) -> h_Omul sz sg
502 | Odiv sz -> h_Odiv sz
503 | Odivu sz -> h_Odivu sz
504 | Omod sz -> h_Omod sz
505 | Omodu sz -> h_Omodu sz
506 | Oand (sz, sg) -> h_Oand sz sg
507 | Oor (sz, sg) -> h_Oor sz sg
508 | Oxor (sz, sg) -> h_Oxor sz sg
509 | Oshl (sz, sg) -> h_Oshl sz sg
510 | Oshr (sz, sg) -> h_Oshr sz sg
511 | Oshru (sz, sg) -> h_Oshru sz sg
512 | Ocmp (sz, sg, sg', x_13454) -> h_Ocmp sz sg sg' x_13454
513 | Ocmpu (sz, sg', x_13455) -> h_Ocmpu sz sg' x_13455
514 | Oaddpi sz -> h_Oaddpi sz
515 | Oaddip sz -> h_Oaddip sz
516 | Osubpi sz -> h_Osubpi sz
517 | Osubpp sz -> h_Osubpp sz
518 | Ocmpp (sg', x_13456) -> h_Ocmpp sg' x_13456
520 (** val binary_operation_rect_Type2 :
521 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
522 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
523 -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
524 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
525 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
526 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
527 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
528 AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
529 (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
530 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
531 (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
532 AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
533 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13479 x_13478 x_13477 = function
534 | Oadd (sz, sg) -> h_Oadd sz sg
535 | Osub (sz, sg) -> h_Osub sz sg
536 | Omul (sz, sg) -> h_Omul sz sg
537 | Odiv sz -> h_Odiv sz
538 | Odivu sz -> h_Odivu sz
539 | Omod sz -> h_Omod sz
540 | Omodu sz -> h_Omodu sz
541 | Oand (sz, sg) -> h_Oand sz sg
542 | Oor (sz, sg) -> h_Oor sz sg
543 | Oxor (sz, sg) -> h_Oxor sz sg
544 | Oshl (sz, sg) -> h_Oshl sz sg
545 | Oshr (sz, sg) -> h_Oshr sz sg
546 | Oshru (sz, sg) -> h_Oshru sz sg
547 | Ocmp (sz, sg, sg', x_13481) -> h_Ocmp sz sg sg' x_13481
548 | Ocmpu (sz, sg', x_13482) -> h_Ocmpu sz sg' x_13482
549 | Oaddpi sz -> h_Oaddpi sz
550 | Oaddip sz -> h_Oaddip sz
551 | Osubpi sz -> h_Osubpi sz
552 | Osubpp sz -> h_Osubpp sz
553 | Ocmpp (sg', x_13483) -> h_Ocmpp sg' x_13483
555 (** val binary_operation_rect_Type1 :
556 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
557 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
558 -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
559 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
560 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
561 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
562 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
563 AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
564 (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
565 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
566 (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
567 AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
568 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13506 x_13505 x_13504 = function
569 | Oadd (sz, sg) -> h_Oadd sz sg
570 | Osub (sz, sg) -> h_Osub sz sg
571 | Omul (sz, sg) -> h_Omul sz sg
572 | Odiv sz -> h_Odiv sz
573 | Odivu sz -> h_Odivu sz
574 | Omod sz -> h_Omod sz
575 | Omodu sz -> h_Omodu sz
576 | Oand (sz, sg) -> h_Oand sz sg
577 | Oor (sz, sg) -> h_Oor sz sg
578 | Oxor (sz, sg) -> h_Oxor sz sg
579 | Oshl (sz, sg) -> h_Oshl sz sg
580 | Oshr (sz, sg) -> h_Oshr sz sg
581 | Oshru (sz, sg) -> h_Oshru sz sg
582 | Ocmp (sz, sg, sg', x_13508) -> h_Ocmp sz sg sg' x_13508
583 | Ocmpu (sz, sg', x_13509) -> h_Ocmpu sz sg' x_13509
584 | Oaddpi sz -> h_Oaddpi sz
585 | Oaddip sz -> h_Oaddip sz
586 | Osubpi sz -> h_Osubpi sz
587 | Osubpp sz -> h_Osubpp sz
588 | Ocmpp (sg', x_13510) -> h_Ocmpp sg' x_13510
590 (** val binary_operation_rect_Type0 :
591 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
592 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
593 -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
594 -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
595 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
596 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
597 -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
598 AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
599 (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
600 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
601 (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
602 AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
603 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13533 x_13532 x_13531 = function
604 | Oadd (sz, sg) -> h_Oadd sz sg
605 | Osub (sz, sg) -> h_Osub sz sg
606 | Omul (sz, sg) -> h_Omul sz sg
607 | Odiv sz -> h_Odiv sz
608 | Odivu sz -> h_Odivu sz
609 | Omod sz -> h_Omod sz
610 | Omodu sz -> h_Omodu sz
611 | Oand (sz, sg) -> h_Oand sz sg
612 | Oor (sz, sg) -> h_Oor sz sg
613 | Oxor (sz, sg) -> h_Oxor sz sg
614 | Oshl (sz, sg) -> h_Oshl sz sg
615 | Oshr (sz, sg) -> h_Oshr sz sg
616 | Oshru (sz, sg) -> h_Oshru sz sg
617 | Ocmp (sz, sg, sg', x_13535) -> h_Ocmp sz sg sg' x_13535
618 | Ocmpu (sz, sg', x_13536) -> h_Ocmpu sz sg' x_13536
619 | Oaddpi sz -> h_Oaddpi sz
620 | Oaddip sz -> h_Oaddip sz
621 | Osubpi sz -> h_Osubpi sz
622 | Osubpp sz -> h_Osubpp sz
623 | Ocmpp (sg', x_13537) -> h_Ocmpp sg' x_13537
625 (** val binary_operation_inv_rect_Type4 :
626 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
627 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
628 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
629 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
630 __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
631 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
632 -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
633 -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
634 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
635 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
636 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
637 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
638 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
639 -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
640 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
641 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
642 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
643 __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
644 __ -> __ -> __ -> 'a1) -> 'a1 **)
645 let binary_operation_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
647 binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
648 h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
652 (** val binary_operation_inv_rect_Type3 :
653 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
654 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
655 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
656 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
657 __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
658 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
659 -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
660 -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
661 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
662 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
663 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
664 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
665 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
666 -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
667 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
668 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
669 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
670 __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
671 __ -> __ -> __ -> 'a1) -> 'a1 **)
672 let binary_operation_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
674 binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
675 h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
679 (** val binary_operation_inv_rect_Type2 :
680 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
681 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
682 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
683 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
684 __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
685 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
686 -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
687 -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
688 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
689 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
690 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
691 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
692 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
693 -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
694 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
695 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
696 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
697 __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
698 __ -> __ -> __ -> 'a1) -> 'a1 **)
699 let binary_operation_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
701 binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
702 h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
706 (** val binary_operation_inv_rect_Type1 :
707 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
708 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
709 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
710 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
711 __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
712 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
713 -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
714 -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
715 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
716 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
717 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
718 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
719 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
720 -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
721 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
722 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
723 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
724 __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
725 __ -> __ -> __ -> 'a1) -> 'a1 **)
726 let binary_operation_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
728 binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
729 h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
733 (** val binary_operation_inv_rect_Type0 :
734 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
735 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
736 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
737 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
738 __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
739 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
740 -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
741 -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
742 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
743 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
744 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
745 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
746 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
747 -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
748 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
749 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
750 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
751 __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
752 __ -> __ -> __ -> 'a1) -> 'a1 **)
753 let binary_operation_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
755 binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
756 h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
760 (** val binary_operation_discr :
761 AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
763 let binary_operation_discr a1 a2 a3 x y =
764 Logic.eq_rect_Type2 x
766 | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
767 | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
768 | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
769 | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
770 | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
771 | Omod a0 -> Obj.magic (fun _ dH -> dH __)
772 | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
773 | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
774 | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
775 | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
776 | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
777 | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
778 | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
779 | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
780 | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
781 | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
782 | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
783 | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
784 | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
785 | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
787 (** val binary_operation_jmdiscr :
788 AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
790 let binary_operation_jmdiscr a1 a2 a3 x y =
791 Logic.eq_rect_Type2 x
793 | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
794 | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
795 | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
796 | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
797 | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
798 | Omod a0 -> Obj.magic (fun _ dH -> dH __)
799 | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
800 | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
801 | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
802 | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
803 | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
804 | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
805 | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
806 | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
807 | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
808 | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
809 | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
810 | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
811 | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
812 | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
814 (** val eval_constant :
815 AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block
816 -> constant -> Values.val0 Types.option **)
817 let eval_constant t find_symbol sp = function
818 | Ointconst (sz, sg, n) -> Types.Some (Values.Vint (sz, n))
819 | Oaddrsymbol (s, ofs) ->
820 (match find_symbol s with
821 | Types.None -> Types.None
823 Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff =
824 (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
825 Pointers.zero_offset (AST.repr AST.I16 ofs)) }))
827 Types.Some (Values.Vptr { Pointers.pblock = sp; Pointers.poff =
828 (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
829 Pointers.zero_offset (AST.repr AST.I16 ofs)) })
832 AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
834 let eval_unop t t' op arg =
836 | Ocastint (sz, sg, sz', sg') ->
838 | AST.Signed -> Types.Some (Values.sign_ext sz' arg)
839 | AST.Unsigned -> Types.Some (Values.zero_ext sz' arg))
840 | Onegint (sz, sg) ->
842 | Values.Vundef -> Types.None
843 | Values.Vint (sz1, n1) ->
844 Types.Some (Values.Vint (sz1,
845 (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz1) n1)))
846 | Values.Vnull -> Types.None
847 | Values.Vptr x -> Types.None)
848 | Onotbool (t0, sz, sg) ->
850 | Values.Vundef -> Types.None
851 | Values.Vint (sz1, n1) ->
852 Types.Some (Values.Vint (sz,
853 (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
854 (BitVector.zero (AST.bitsize_of_intsize sz1)) with
855 | Bool.True -> AST.repr sz (Nat.S Nat.O)
856 | Bool.False -> BitVector.zero (AST.bitsize_of_intsize sz))))
858 Types.Some (Values.Vint (sz, (AST.repr sz (Nat.S Nat.O))))
860 Types.Some (Values.Vint (sz,
861 (BitVector.zero (AST.bitsize_of_intsize sz)))))
862 | Onotint (sz, sg) ->
864 | Values.Vundef -> Types.None
865 | Values.Vint (sz1, n1) ->
866 Types.Some (Values.Vint (sz1,
867 (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz1) n1
869 | Values.Vnull -> Types.None
870 | Values.Vptr x -> Types.None)
871 | Oid t0 -> Types.Some arg
872 | Optrofint (sz, sg) ->
874 | Values.Vundef -> Types.None
875 | Values.Vint (sz1, n1) ->
876 (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
877 (BitVector.zero (AST.bitsize_of_intsize sz1)) with
878 | Bool.True -> Types.Some Values.Vnull
879 | Bool.False -> Types.None)
880 | Values.Vnull -> Types.None
881 | Values.Vptr x -> Types.None)
882 | Ointofptr (sz, sg) ->
884 | Values.Vundef -> Types.None
885 | Values.Vint (x, x0) -> Types.None
887 Types.Some (Values.Vint (sz,
888 (BitVector.zero (AST.bitsize_of_intsize sz))))
889 | Values.Vptr x -> Types.None)
891 (** val eval_compare_mismatch :
892 Integers.comparison -> Values.val0 Types.option **)
893 let eval_compare_mismatch = function
894 | Integers.Ceq -> Types.Some Values.vfalse
895 | Integers.Cne -> Types.Some Values.vtrue
896 | Integers.Clt -> Types.None
897 | Integers.Cle -> Types.None
898 | Integers.Cgt -> Types.None
899 | Integers.Cge -> Types.None
901 (** val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
904 | Values.Vundef -> Types.None
905 | Values.Vint (sz1, n1) ->
907 | Values.Vundef -> Types.None
908 | Values.Vint (sz2, n2) ->
909 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
910 (sz2, (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
912 | Values.Vnull -> Types.None
913 | Values.Vptr x -> Types.None)
914 | Values.Vnull -> Types.None
915 | Values.Vptr x -> Types.None
917 (** val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
920 | Values.Vundef -> Types.None
921 | Values.Vint (sz1, n1) ->
923 | Values.Vundef -> Types.None
924 | Values.Vint (sz2, n2) ->
925 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
927 (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
929 | Values.Vnull -> Types.None
930 | Values.Vptr x -> Types.None)
931 | Values.Vnull -> Types.None
932 | Values.Vptr x -> Types.None
934 (** val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
937 | Values.Vundef -> Types.None
938 | Values.Vint (x, x0) -> Types.None
941 | Values.Vundef -> Types.None
942 | Values.Vint (sz2, n2) ->
943 (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
944 (BitVector.zero (AST.bitsize_of_intsize sz2)) with
945 | Bool.True -> Types.Some Values.Vnull
946 | Bool.False -> Types.None)
947 | Values.Vnull -> Types.None
948 | Values.Vptr x -> Types.None)
949 | Values.Vptr ptr1 ->
951 | Values.Vundef -> Types.None
952 | Values.Vint (sz2, n2) ->
953 Types.Some (Values.Vptr
954 (Pointers.shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
955 | Values.Vnull -> Types.None
956 | Values.Vptr x -> Types.None)
958 (** val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
961 | Values.Vundef -> Types.None
962 | Values.Vint (x, x0) -> Types.None
965 | Values.Vundef -> Types.None
966 | Values.Vint (sz2, n2) ->
967 (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
968 (BitVector.zero (AST.bitsize_of_intsize sz2)) with
969 | Bool.True -> Types.Some Values.Vnull
970 | Bool.False -> Types.None)
971 | Values.Vnull -> Types.None
972 | Values.Vptr x -> Types.None)
973 | Values.Vptr ptr1 ->
975 | Values.Vundef -> Types.None
976 | Values.Vint (sz2, n2) ->
977 Types.Some (Values.Vptr
978 (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
979 | Values.Vnull -> Types.None
980 | Values.Vptr x -> Types.None)
983 AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option **)
984 let ev_subpp sz v1 v2 =
986 | Values.Vundef -> Types.None
987 | Values.Vint (x, x0) -> Types.None
990 | Values.Vundef -> Types.None
991 | Values.Vint (x, x0) -> Types.None
993 Types.Some (Values.Vint (sz,
994 (BitVector.zero (AST.bitsize_of_intsize sz))))
995 | Values.Vptr x -> Types.None)
996 | Values.Vptr ptr1 ->
998 | Values.Vundef -> Types.None
999 | Values.Vint (x, x0) -> Types.None
1000 | Values.Vnull -> Types.None
1001 | Values.Vptr ptr2 ->
1002 (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
1004 Types.Some (Values.Vint (sz,
1005 (Pointers.sub_offset (AST.bitsize_of_intsize sz)
1006 ptr1.Pointers.poff ptr2.Pointers.poff)))
1007 | Bool.False -> Types.None))
1009 (** val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1012 | Values.Vundef -> Types.None
1013 | Values.Vint (sz1, n1) ->
1015 | Values.Vundef -> Types.None
1016 | Values.Vint (sz2, n2) ->
1017 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1019 (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
1021 | Values.Vnull -> Types.None
1022 | Values.Vptr x -> Types.None)
1023 | Values.Vnull -> Types.None
1024 | Values.Vptr x -> Types.None
1026 (** val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1029 | Values.Vundef -> Types.None
1030 | Values.Vint (sz1, n1) ->
1032 | Values.Vundef -> Types.None
1033 | Values.Vint (sz2, n2) ->
1034 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1035 Types.option_map (fun x -> Values.Vint (sz2, x))
1036 (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
1038 | Values.Vnull -> Types.None
1039 | Values.Vptr x -> Types.None)
1040 | Values.Vnull -> Types.None
1041 | Values.Vptr x -> Types.None
1043 (** val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1046 | Values.Vundef -> Types.None
1047 | Values.Vint (sz1, n1) ->
1049 | Values.Vundef -> Types.None
1050 | Values.Vint (sz2, n2) ->
1051 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1052 Types.option_map (fun x -> Values.Vint (sz2, x))
1053 (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
1055 | Values.Vnull -> Types.None
1056 | Values.Vptr x -> Types.None)
1057 | Values.Vnull -> Types.None
1058 | Values.Vptr x -> Types.None
1060 (** val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1063 | Values.Vundef -> Types.None
1064 | Values.Vint (sz1, n1) ->
1066 | Values.Vundef -> Types.None
1067 | Values.Vint (sz2, n2) ->
1068 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1069 Types.option_map (fun x -> Values.Vint (sz2, x))
1070 (Arithmetic.division_u
1071 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1073 (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1074 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1076 | Values.Vnull -> Types.None
1077 | Values.Vptr x -> Types.None)
1078 | Values.Vnull -> Types.None
1079 | Values.Vptr x -> Types.None
1081 (** val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1084 | Values.Vundef -> Types.None
1085 | Values.Vint (sz1, n1) ->
1087 | Values.Vundef -> Types.None
1088 | Values.Vint (sz2, n2) ->
1089 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1090 Types.option_map (fun x -> Values.Vint (sz2, x))
1091 (Arithmetic.modulus_u
1092 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1094 (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1095 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1097 | Values.Vnull -> Types.None
1098 | Values.Vptr x -> Types.None)
1099 | Values.Vnull -> Types.None
1100 | Values.Vptr x -> Types.None
1102 (** val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1105 | Values.Vundef -> Types.None
1106 | Values.Vint (sz1, n1) ->
1108 | Values.Vundef -> Types.None
1109 | Values.Vint (sz2, n2) ->
1110 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1112 (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
1114 | Values.Vnull -> Types.None
1115 | Values.Vptr x -> Types.None)
1116 | Values.Vnull -> Types.None
1117 | Values.Vptr x -> Types.None
1119 (** val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1122 | Values.Vundef -> Types.None
1123 | Values.Vint (sz1, n1) ->
1125 | Values.Vundef -> Types.None
1126 | Values.Vint (sz2, n2) ->
1127 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1129 (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1131 | Values.Vnull -> Types.None
1132 | Values.Vptr x -> Types.None)
1133 | Values.Vnull -> Types.None
1134 | Values.Vptr x -> Types.None
1136 (** val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1139 | Values.Vundef -> Types.None
1140 | Values.Vint (sz1, n1) ->
1142 | Values.Vundef -> Types.None
1143 | Values.Vint (sz2, n2) ->
1144 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1146 (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1148 | Values.Vnull -> Types.None
1149 | Values.Vptr x -> Types.None)
1150 | Values.Vnull -> Types.None
1151 | Values.Vptr x -> Types.None
1153 (** val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1156 | Values.Vundef -> Types.None
1157 | Values.Vint (sz1, n1) ->
1159 | Values.Vundef -> Types.None
1160 | Values.Vint (sz2, n2) ->
1161 (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1162 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1163 (AST.bitsize_of_intsize sz1)) with
1165 Types.Some (Values.Vint (sz1,
1166 (Vector.shift_left (AST.bitsize_of_intsize sz1)
1167 (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1169 | Bool.False -> Types.None)
1170 | Values.Vnull -> Types.None
1171 | Values.Vptr x -> Types.None)
1172 | Values.Vnull -> Types.None
1173 | Values.Vptr x -> Types.None
1175 (** val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1178 | Values.Vundef -> Types.None
1179 | Values.Vint (sz1, n1) ->
1181 | Values.Vundef -> Types.None
1182 | Values.Vint (sz2, n2) ->
1183 (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1184 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1185 (AST.bitsize_of_intsize sz1)) with
1187 Types.Some (Values.Vint (sz1,
1189 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1191 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1192 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1193 (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1196 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1198 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1199 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n1))))
1200 | Bool.False -> Types.None)
1201 | Values.Vnull -> Types.None
1202 | Values.Vptr x -> Types.None)
1203 | Values.Vnull -> Types.None
1204 | Values.Vptr x -> Types.None
1206 (** val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1209 | Values.Vundef -> Types.None
1210 | Values.Vint (sz1, n1) ->
1212 | Values.Vundef -> Types.None
1213 | Values.Vint (sz2, n2) ->
1214 (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1215 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1216 (AST.bitsize_of_intsize sz1)) with
1218 Types.Some (Values.Vint (sz1,
1220 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1222 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1223 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1224 (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1226 | Bool.False -> Types.None)
1227 | Values.Vnull -> Types.None
1228 | Values.Vptr x -> Types.None)
1229 | Values.Vnull -> Types.None
1230 | Values.Vptr x -> Types.None
1232 (** val fEtrue : Values.val0 **)
1234 Values.Vint (AST.I8, (AST.repr AST.I8 (Nat.S Nat.O)))
1236 (** val fEfalse : Values.val0 **)
1238 Values.Vint (AST.I8, (AST.repr AST.I8 Nat.O))
1240 (** val fE_of_bool : Bool.bool -> Values.val0 **)
1241 let fE_of_bool = function
1242 | Bool.True -> fEtrue
1243 | Bool.False -> fEfalse
1245 (** val ev_cmp_match : Integers.comparison -> Values.val0 Types.option **)
1246 let ev_cmp_match = function
1247 | Integers.Ceq -> Types.Some fEtrue
1248 | Integers.Cne -> Types.Some fEfalse
1249 | Integers.Clt -> Types.None
1250 | Integers.Cle -> Types.None
1251 | Integers.Cgt -> Types.None
1252 | Integers.Cge -> Types.None
1254 (** val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option **)
1255 let ev_cmp_mismatch = function
1256 | Integers.Ceq -> Types.Some fEfalse
1257 | Integers.Cne -> Types.Some fEtrue
1258 | Integers.Clt -> Types.None
1259 | Integers.Cle -> Types.None
1260 | Integers.Cgt -> Types.None
1261 | Integers.Cge -> Types.None
1264 Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1266 let ev_cmp c v1 v2 =
1268 | Values.Vundef -> Types.None
1269 | Values.Vint (sz1, n1) ->
1271 | Values.Vundef -> Types.None
1272 | Values.Vint (sz2, n2) ->
1273 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1274 (fE_of_bool (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1276 | Values.Vnull -> Types.None
1277 | Values.Vptr x -> Types.None)
1278 | Values.Vnull -> Types.None
1279 | Values.Vptr x -> Types.None
1282 GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
1283 Values.val0 Types.option **)
1284 let ev_cmpp m c v1 v2 =
1286 | Values.Vundef -> Types.None
1287 | Values.Vint (x, x0) -> Types.None
1290 | Values.Vundef -> Types.None
1291 | Values.Vint (x, x0) -> Types.None
1292 | Values.Vnull -> ev_cmp_match c
1293 | Values.Vptr x -> ev_cmp_mismatch c)
1294 | Values.Vptr ptr1 ->
1296 | Values.Vundef -> Types.None
1297 | Values.Vint (x, x0) -> Types.None
1298 | Values.Vnull -> ev_cmp_mismatch c
1299 | Values.Vptr ptr2 ->
1300 (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
1301 (FrontEndMem.valid_pointer m ptr2) with
1303 (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
1307 (Values.cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff))
1308 | Bool.False -> ev_cmp_mismatch c)
1309 | Bool.False -> Types.None))
1312 Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1314 let ev_cmpu c v1 v2 =
1316 | Values.Vundef -> Types.None
1317 | Values.Vint (sz1, n1) ->
1319 | Values.Vundef -> Types.None
1320 | Values.Vint (sz2, n2) ->
1321 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1322 (fE_of_bool (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1324 | Values.Vnull -> Types.None
1325 | Values.Vptr x -> Types.None)
1326 | Values.Vnull -> Types.None
1327 | Values.Vptr x -> Types.None
1329 (** val eval_binop :
1330 GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
1331 Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1332 let eval_binop m t1 t2 t' = function
1333 | Oadd (x, x0) -> ev_add
1334 | Osub (x, x0) -> ev_sub
1335 | Omul (x, x0) -> ev_mul
1337 | Odivu x -> ev_divu
1339 | Omodu x -> ev_modu
1340 | Oand (x, x0) -> ev_and
1341 | Oor (x, x0) -> ev_or
1342 | Oxor (x, x0) -> ev_xor
1343 | Oshl (x, x0) -> ev_shl
1344 | Oshr (x, x0) -> ev_shr
1345 | Oshru (x, x0) -> ev_shru
1346 | Ocmp (x, x0, x1, c) -> ev_cmp c
1347 | Ocmpu (x, x0, c) -> ev_cmpu c
1348 | Oaddpi x -> ev_addpi
1349 | Oaddip x -> (fun x0 y -> ev_addpi y x0)
1350 | Osubpi x -> ev_subpi
1351 | Osubpp sz -> ev_subpp sz
1352 | Ocmpp (x, c) -> ev_cmpp m c