Skip to content

Commit

Permalink
Merge branch 'master' into goblint-dune-libs-3
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Dec 29, 2023
2 parents 7ee115a + b671ffa commit cedbc19
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 95 deletions.
93 changes: 0 additions & 93 deletions src/cdomain/value/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 0 additions & 2 deletions src/cdomain/value/cdomains/intDomain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit cedbc19

Please sign in to comment.