Skip to content

Commit f8627f1

Browse files
committed
Replace Goblintutil.opt_predicate -> GobOption.exists
1 parent edadcab commit f8627f1

File tree

4 files changed

+7
-12
lines changed

4 files changed

+7
-12
lines changed

src/analyses/base.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ struct
199199
| `NoOffset -> `Index(iDtoIdx n, `NoOffset)
200200
in
201201
let default = function
202-
| Addr.NullPtr when GU.opt_predicate (BI.equal BI.zero) (ID.to_int n) -> Addr.NullPtr
202+
| Addr.NullPtr when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> Addr.NullPtr
203203
| _ -> Addr.UnknownPtr
204204
in
205205
match Addr.to_var_offset addr with
@@ -1458,7 +1458,7 @@ struct
14581458
(* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *)
14591459
let inv_bin_int (a, b) ikind c op =
14601460
let warn_and_top_on_zero x =
1461-
if GU.opt_predicate (BI.equal BI.zero) (ID.to_int x) then
1461+
if GobOption.exists (BI.equal BI.zero) (ID.to_int x) then
14621462
(M.warn "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
14631463
ID.top_of ikind)
14641464
else
@@ -2210,7 +2210,7 @@ struct
22102210
| `ThreadJoin (id,ret_var) ->
22112211
let st' =
22122212
match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with
2213-
| `Int n when GU.opt_predicate (BI.equal BI.zero) (ID.to_int n) -> st
2213+
| `Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
22142214
| `Address ret_a ->
22152215
begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
22162216
| `Thread a ->

src/cdomains/addressDomain.ml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
open Cil
22
open Pretty
3-
open Goblintutil
43
open IntOps
54
let fast_addr_sets = false (* unknown addresses for fast sets == top, for slow == {?}*)
65

@@ -52,8 +51,8 @@ struct
5251

5352
let of_int (type a) (module ID : IntDomain.Z with type t = a) i =
5453
match ID.to_int i with
55-
| x when opt_predicate BigIntOps.(equal (zero)) x -> null_ptr
56-
| x when opt_predicate BigIntOps.(equal (one)) x -> not_null
54+
| x when GobOption.exists BigIntOps.(equal (zero)) x -> null_ptr
55+
| x when GobOption.exists BigIntOps.(equal (one)) x -> not_null
5756
| _ -> match ID.to_excl_list i with
5857
| Some xs when List.exists BigIntOps.(equal (zero)) xs -> not_null
5958
| _ -> top_ptr

src/cdomains/valueDomain.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -860,7 +860,7 @@ struct
860860
begin
861861
do_eval_offset ask f x offs exp l' o' v t (* this used to be `blob `address -> we ignore the index *)
862862
end
863-
| x when Goblintutil.opt_predicate (BI.equal (BI.zero)) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
863+
| x when GobOption.exists (BI.equal (BI.zero)) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
864864
| `Top -> M.debug "Trying to read an index, but the array is unknown"; top ()
865865
| _ -> M.warn "Trying to read an index, but was not given an array (%a)" pretty x; top ()
866866
end
@@ -998,7 +998,7 @@ struct
998998
let new_array_value = CArrays.update_length newl new_array_value in
999999
`Array new_array_value
10001000
| `Top -> M.warn "Trying to update an index, but the array is unknown"; top ()
1001-
| x when Goblintutil.opt_predicate (BI.equal BI.zero) (IndexDomain.to_int idx) -> do_update_offset ask x offs value exp l' o' v t
1001+
| x when GobOption.exists (BI.equal BI.zero) (IndexDomain.to_int idx) -> do_update_offset ask x offs value exp l' o' v t
10021002
| _ -> M.warn "Trying to update an index, but was not given an array(%a)" pretty x; top ()
10031003
end
10041004
in mu result

src/util/goblintutil.ml

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -157,10 +157,6 @@ let arinc_time_capacity = if scrambled then "M166" else "TIME_CAPACITY"
157157
let exe_dir = Filename.dirname Sys.executable_name
158158
let command = String.concat " " (Array.to_list Sys.argv)
159159

160-
let opt_predicate (f : 'a -> bool) = function
161-
| Some x -> f x
162-
| None -> false
163-
164160
(* https://ocaml.org/api/Sys.html#2_SignalnumbersforthestandardPOSIXsignals *)
165161
(* https://ocaml.github.io/ocamlunix/signals.html *)
166162
let signal_of_string = let open Sys in function

0 commit comments

Comments
 (0)