|
282 | 282 |
|
283 | 283 | module type Z = Y with type int_t = BI.t |
284 | 284 |
|
285 | | -module OldDomainFacade (Old : IkindUnawareS with type int_t = int64) : S with type int_t = BI.t and type t = Old.t = |
286 | | -struct |
287 | | - include Old |
288 | | - type int_t = BI.t |
289 | | - let neg ?no_ov _ik = Old.neg |
290 | | - let add ?no_ov _ik = Old.add |
291 | | - let sub ?no_ov _ik = Old.sub |
292 | | - let mul ?no_ov _ik = Old.mul |
293 | | - let div ?no_ov _ik = Old.div |
294 | | - let rem _ik = Old.rem |
295 | | - |
296 | | - let lt _ik = Old.lt |
297 | | - let gt _ik = Old.gt |
298 | | - let le _ik = Old.le |
299 | | - let ge _ik = Old.ge |
300 | | - let eq _ik = Old.eq |
301 | | - let ne _ik = Old.ne |
302 | | - |
303 | | - let bitnot _ik = bitnot |
304 | | - let bitand _ik = bitand |
305 | | - let bitor _ik = bitor |
306 | | - let bitxor _ik = bitxor |
307 | | - |
308 | | - let shift_left _ik = shift_left |
309 | | - let shift_right _ik = shift_right |
310 | | - |
311 | | - let lognot _ik = lognot |
312 | | - let logand _ik = logand |
313 | | - let logor _ik = logor |
314 | | - |
315 | | - |
316 | | - let to_int a = Option.map BI.of_int64 (Old.to_int a) |
317 | | - |
318 | | - let equal_to (x: int_t) (a: t)= |
319 | | - try |
320 | | - Old.equal_to (BI.to_int64 x) a |
321 | | - with Z.Overflow | Failure _ -> `Top |
322 | | - |
323 | | - let to_excl_list a = Option.map (BatTuple.Tuple2.map1 (List.map BI.of_int64)) (Old.to_excl_list a) |
324 | | - let of_excl_list ik xs = |
325 | | - let xs' = List.map BI.to_int64 xs in |
326 | | - Old.of_excl_list ik xs' |
327 | | - |
328 | | - let to_incl_list a = Option.map (List.map BI.of_int64) (Old.to_incl_list a) |
329 | | - |
330 | | - let maximal a = Option.map BI.of_int64 (Old.maximal a) |
331 | | - let minimal a = Option.map BI.of_int64 (Old.minimal a) |
332 | | - |
333 | | - let of_int ik x = |
334 | | - (* If we cannot convert x to int64, we have to represent it with top in the underlying domain*) |
335 | | - try |
336 | | - Old.of_int (BI.to_int64 x) |
337 | | - with |
338 | | - Failure _ -> top_of ik |
339 | | - |
340 | | - let of_bool ik b = Old.of_bool b |
341 | | - let of_interval ?(suppress_ovwarn=false) ik (l, u) = |
342 | | - try |
343 | | - Old.of_interval ~suppress_ovwarn ik (BI.to_int64 l, BI.to_int64 u) |
344 | | - with |
345 | | - Failure _ -> top_of ik |
346 | | - let of_congruence ik (c, m) = |
347 | | - try |
348 | | - Old.of_congruence ik (BI.to_int64 c, BI.to_int64 m) |
349 | | - with |
350 | | - Failure _ -> top_of ik |
351 | | - |
352 | | - let starting ?(suppress_ovwarn=false) ik x = |
353 | | - try Old.starting ~suppress_ovwarn ik (BI.to_int64 x) with Failure _ -> top_of ik |
354 | | - let ending ?(suppress_ovwarn=false) ik x = |
355 | | - try Old.ending ~suppress_ovwarn ik (BI.to_int64 x) with Failure _ -> top_of ik |
356 | | - |
357 | | - let join _ik = Old.join |
358 | | - let meet _ik = Old.meet |
359 | | - let narrow _ik = Old.narrow |
360 | | - let widen _ik = Old.widen |
361 | | - |
362 | | - let is_top_of _ik = Old.is_top |
363 | | - |
364 | | - let invariant_ikind e ik t = Old.invariant e t |
365 | | - |
366 | | - let cast_to ?torg ?no_ov = Old.cast_to ?torg |
367 | | - |
368 | | - let refine_with_congruence ik a b = a |
369 | | - let refine_with_interval ik a b = a |
370 | | - let refine_with_excl_list ik a b = a |
371 | | - let refine_with_incl_list ik a b = a |
372 | | - |
373 | | - let project ik p t = t |
374 | | - |
375 | | - let arbitrary _ik = Old.arbitrary () |
376 | | -end |
377 | | - |
378 | 285 |
|
379 | 286 | module IntDomLifter (I : S) = |
380 | 287 | struct |
|
0 commit comments