Skip to content

Commit 5da3024

Browse files
Remove custom default function from arrayDomain
1 parent 2812ce7 commit 5da3024

File tree

1 file changed

+4
-7
lines changed

1 file changed

+4
-7
lines changed

src/cdomain/value/cdomains/arrayDomain.ml

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -202,9 +202,6 @@ struct
202202
(show_list xl) ^ Val.show xr ^ ")"
203203
let pretty () x = text "Array: " ++ text (show x)
204204
let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
205-
let extract x default = match x with
206-
| Some c -> c
207-
| None -> default
208205
let get ?(checkBounds=true) (ask: VDQ.t) (xl, xr) (_,i) =
209206
let search_unrolled_values min_i max_i =
210207
let rec subjoin l i = match l with
@@ -218,8 +215,8 @@ struct
218215
end in
219216
subjoin xl Z.zero in
220217
let f = Z.of_int (factor ()) in
221-
let min_i = extract (Idx.minimal i) Z.zero in
222-
let max_i = extract (Idx.maximal i) f in
218+
let min_i = BatOption.default Z.zero (Idx.minimal i) in
219+
let max_i = BatOption.default f (Idx.maximal i) in
223220
if Z.geq min_i f then xr
224221
else if Z.lt max_i f then search_unrolled_values min_i max_i
225222
else Val.join xr (search_unrolled_values min_i (Z.of_int ((factor ())-1)))
@@ -239,8 +236,8 @@ struct
239236
if Z.equal min_i max_i then full_update xl Z.zero
240237
else weak_update xl Z.zero in
241238
let f = Z.of_int (factor ()) in
242-
let min_i = extract(Idx.minimal i) Z.zero in
243-
let max_i = extract(Idx.maximal i) f in
239+
let min_i = BatOption.default Z.zero (Idx.minimal i) in
240+
let max_i = BatOption.default f (Idx.maximal i) in
244241
if Z.geq min_i f then (xl, (Val.join xr v))
245242
else if Z.lt max_i f then ((update_unrolled_values min_i max_i), xr)
246243
else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))

0 commit comments

Comments
 (0)