diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 376dab71c2..986634066c 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -282,99 +282,6 @@ end module type Z = Y with type int_t = BI.t -module OldDomainFacade (Old : IkindUnawareS with type int_t = int64) : S with type int_t = BI.t and type t = Old.t = -struct - include Old - type int_t = BI.t - let neg ?no_ov _ik = Old.neg - let add ?no_ov _ik = Old.add - let sub ?no_ov _ik = Old.sub - let mul ?no_ov _ik = Old.mul - let div ?no_ov _ik = Old.div - let rem _ik = Old.rem - - let lt _ik = Old.lt - let gt _ik = Old.gt - let le _ik = Old.le - let ge _ik = Old.ge - let eq _ik = Old.eq - let ne _ik = Old.ne - - let bitnot _ik = bitnot - let bitand _ik = bitand - let bitor _ik = bitor - let bitxor _ik = bitxor - - let shift_left _ik = shift_left - let shift_right _ik = shift_right - - let lognot _ik = lognot - let logand _ik = logand - let logor _ik = logor - - - let to_int a = Option.map BI.of_int64 (Old.to_int a) - - let equal_to (x: int_t) (a: t)= - try - Old.equal_to (BI.to_int64 x) a - with Z.Overflow | Failure _ -> `Top - - let to_excl_list a = Option.map (BatTuple.Tuple2.map1 (List.map BI.of_int64)) (Old.to_excl_list a) - let of_excl_list ik xs = - let xs' = List.map BI.to_int64 xs in - Old.of_excl_list ik xs' - - let to_incl_list a = Option.map (List.map BI.of_int64) (Old.to_incl_list a) - - let maximal a = Option.map BI.of_int64 (Old.maximal a) - let minimal a = Option.map BI.of_int64 (Old.minimal a) - - let of_int ik x = - (* If we cannot convert x to int64, we have to represent it with top in the underlying domain*) - try - Old.of_int (BI.to_int64 x) - with - Failure _ -> top_of ik - - let of_bool ik b = Old.of_bool b - let of_interval ?(suppress_ovwarn=false) ik (l, u) = - try - Old.of_interval ~suppress_ovwarn ik (BI.to_int64 l, BI.to_int64 u) - with - Failure _ -> top_of ik - let of_congruence ik (c, m) = - try - Old.of_congruence ik (BI.to_int64 c, BI.to_int64 m) - with - Failure _ -> top_of ik - - let starting ?(suppress_ovwarn=false) ik x = - try Old.starting ~suppress_ovwarn ik (BI.to_int64 x) with Failure _ -> top_of ik - let ending ?(suppress_ovwarn=false) ik x = - try Old.ending ~suppress_ovwarn ik (BI.to_int64 x) with Failure _ -> top_of ik - - let join _ik = Old.join - let meet _ik = Old.meet - let narrow _ik = Old.narrow - let widen _ik = Old.widen - - let is_top_of _ik = Old.is_top - - let invariant_ikind e ik t = Old.invariant e t - - let cast_to ?torg ?no_ov = Old.cast_to ?torg - - let refine_with_congruence ik a b = a - let refine_with_interval ik a b = a - let refine_with_excl_list ik a b = a - let refine_with_incl_list ik a b = a - - let project ik p t = t - - let arbitrary _ik = Old.arbitrary () -end - module IntDomLifter (I : S) = struct diff --git a/src/cdomains/intDomain.mli b/src/cdomains/intDomain.mli index a853c8acca..4b14aeec72 100644 --- a/src/cdomains/intDomain.mli +++ b/src/cdomains/intDomain.mli @@ -308,8 +308,6 @@ end module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type t = D.t -module OldDomainFacade (Old : IkindUnawareS with type int_t = int64) : S with type int_t = IntOps.BigIntOps.t and type t = Old.t -(** Facade for IntDomain implementations that do not implement the interface where arithmetic functions take an ikind parameter. *) module type Y = sig