Skip to content

Commit

Permalink
Re-use of Interval.invariant_ikind
Browse files Browse the repository at this point in the history
As suggested from the conversation: goblint#966 (comment)
  • Loading branch information
gabryon99 authored and BilelGho committed Jan 26, 2023
1 parent f76da67 commit 1d18378
Showing 1 changed file with 4 additions and 16 deletions.
20 changes: 4 additions & 16 deletions src/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1291,27 +1291,15 @@ struct

let maximal xs = xs |> List.rev |> (function [] -> None | (_, y)::_ -> Some y)

let of_interval ik (x, y) = norm ik @@ Some (x, y)
let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm ik @@ Some (x,y)

let of_int ik (x: int_t) = of_interval ik (x, x)

let of_bool _ik = function true -> one | false -> zero

let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm ik @@ Some (x,y)

let invariant_ikind_interval e ik x = match x with
| (x1, x2) when Ints_t.compare x1 x2 = 0 ->
let x1 = Ints_t.to_bigint x1 in
Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x1, intType))
| (x1, x2) ->
let open Invariant in
let (min_ik, max_ik) = range ik in
let (x1', x2') = BatTuple.Tuple2.mapn (Ints_t.to_bigint) (x1, x2) in
let i1 = if Ints_t.compare min_ik x1 <> 0 then of_exp Cil.(BinOp (Le, kintegerCilint ik x1', e, intType)) else none in
let i2 = if Ints_t.compare x2 max_ik <> 0 then of_exp Cil.(BinOp (Le, e, kintegerCilint ik x2', intType)) else none in
i1 && i2

let invariant_ikind e ik xs = List.map (invariant_ikind_interval e ik) xs |> let open Invariant in List.fold_left (||) (bot ())
let invariant_ikind e ik xs =
List.map (fun x -> Interval_functor.invariant_ikind e ik (Some x)) xs |>
let open Invariant in List.fold_left (||) (bot ())

let modulo n k =
let result = Ints_t.rem n k in
Expand Down

0 comments on commit 1d18378

Please sign in to comment.