Skip to content

Commit

Permalink
Renaming norm function into norm_interval
Browse files Browse the repository at this point in the history
See discussion: goblint#966 (comment)
  • Loading branch information
gabryon99 committed Jan 24, 2023
1 parent a5c65ff commit f000e6c
Showing 1 changed file with 10 additions and 10 deletions.
20 changes: 10 additions & 10 deletions src/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1032,7 +1032,7 @@ struct

include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)

let norm ?(cast=false) ik = function
let norm_interval ?(cast=false) ik = function
| None -> []
| Some (x,y) ->
if Ints_t.compare x y > 0 then
Expand Down Expand Up @@ -1226,7 +1226,7 @@ struct
binary_op ik x y (wrap_binary_interval_function Interval.rem ik)

let cast_to ?torg ?no_ov ik x =
List.map (fun x -> norm ~cast:true ik (Some x)) x |> List.flatten |> canonize
List.map (fun x -> norm_interval ~cast:true ik (Some x)) x |> List.flatten |> canonize

let rec interval_sets_to_partitions (ik: ikind) (acc : (int_t * int_t) option) (xs: t) (ys: t)=
match xs,ys with
Expand Down Expand Up @@ -1314,17 +1314,17 @@ struct
|> List.rev
|> List.map snd

let starting ik n = norm ik @@ Some (n, snd (range ik))
let starting ik n = norm_interval ik @@ Some (n, snd (range ik))

let ending ik n = norm ik @@ Some (fst (range ik), n)
let ending ik n = norm_interval ik @@ Some (fst (range ik), n)

let minimal = function [] -> None | (x, _)::_ -> Some x

let maximal = function
| [] -> None
| xs -> let last = BatList.last xs |> snd in Some last

let of_interval ik (x, y) = norm ik @@ Some (x, y)
let of_interval ik (x, y) = norm_interval ik @@ Some (x, y)

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

Expand Down Expand Up @@ -1353,8 +1353,8 @@ struct
if Ints_t.equal y max_ik then y else
Ints_t.sub y (modulo (Ints_t.sub y c) (Ints_t.abs m)) in
if Ints_t.compare rcx lcy > 0 then []
else if Ints_t.equal rcx lcy then norm ik @@ Some (rcx, rcx)
else norm ik @@ Some (rcx, lcy)
else if Ints_t.equal rcx lcy then norm_interval ik @@ Some (rcx, rcx)
else norm_interval ik @@ Some (rcx, lcy)
| _ -> []
in
List.map (fun x -> Some x) intvs |> List.map (refine_with_congruence_interval ik cong) |> List.flatten
Expand All @@ -1366,8 +1366,8 @@ struct
| Some xs -> meet ik intvs (List.map (fun x -> (x,x)) xs)

let excl_range_to_intervalset (ik: ikind) ((min, max): int_t * int_t) (excl: int_t): t =
let intv1 = norm ik @@ Some (min, Ints_t.sub excl Ints_t.one) in
let intv2 = norm ik @@ Some (Ints_t.add excl Ints_t.one, max) in
let intv1 = norm_interval ik @@ Some (min, Ints_t.sub excl Ints_t.one) in
let intv2 = norm_interval ik @@ Some (Ints_t.add excl Ints_t.one, max) in
intv1 @ intv2

let of_excl_list ik (excls: int_t list) =
Expand All @@ -1392,7 +1392,7 @@ struct
let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
let pair_arb = QCheck.pair int_arb int_arb in
let list_pair_arb = QCheck.small_list pair_arb in
let canonize_randomly_generated_list = fun x -> List.map (fun x -> Some x) x |> List.map (norm ik) |> List.flatten |> canonize in
let canonize_randomly_generated_list = fun x -> List.map (fun x -> Some x) x |> List.map (norm_interval ik) |> List.flatten |> canonize in
let shrink xs = MyCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
in QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) canonize_randomly_generated_list list_pair_arb)

Expand Down

0 comments on commit f000e6c

Please sign in to comment.