diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 0f5f0e1434..82939a144e 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -465,17 +465,15 @@ struct (* Give the set of reachables from argument. *) let reachables (ask: Queries.ask) es = - let reachable e st = - match st with - | None -> None - | Some st -> + let reachable acc e = + Option.bind acc (fun st -> let ad = ask.f (Queries.ReachableFrom e) in if Queries.AD.is_top ad then None else - Some (Queries.AD.join ad st) + Some (Queries.AD.join ad st)) in - List.fold_right reachable es (Some (Queries.AD.empty ())) + List.fold_left reachable (Some (Queries.AD.empty ())) es let forget_reachable man st es = diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c21051b87b..e4288d05b8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -518,7 +518,7 @@ struct (* From a list of values, presumably arguments to a function, simply extract * the pointer arguments. *) let get_ptrs (vals: value list): address list = - let f (x:value) acc = match x with + let f acc (x:value) = match x with | Address adrs when AD.is_top adrs -> M.info ~category:Unsound "Unknown address given as function argument"; acc | Address adrs when AD.to_var_may adrs = [] -> acc @@ -528,7 +528,7 @@ struct | Top -> M.info ~category:Unsound "Unknown value type given as function argument"; acc | _ -> acc in - List.fold_right f vals [] + List.fold_left f [] vals let rec reachable_from_value ask (value: value) (t: typ) (description: string) = let empty = AD.empty () in @@ -572,7 +572,7 @@ struct if M.tracing then M.traceli "reachability" "Checking reachable arguments from [%a]!" (d_list ", " AD.pretty) args; let empty = AD.empty () in (* We begin looking at the parameters: *) - let argset = List.fold_right (AD.join) args empty in + let argset = List.fold_left (AD.join) empty args in let workset = ref argset in (* And we keep a set of already visited variables *) let visited = ref empty in diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml index 07f798583e..edd5e2e8d9 100644 --- a/src/analyses/malloc_null.ml +++ b/src/analyses/malloc_null.ml @@ -94,7 +94,7 @@ struct (* Remove null values from state that are unreachable from exp.*) let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t = let reachable = - let do_exp e a = + let do_exp a e = match ask.f (Queries.ReachableFrom e) with | ad when not (Queries.AD.is_top ad) -> ad @@ -103,9 +103,9 @@ struct | _ -> false) |> Queries.AD.join a (* Ignore soundness warnings, as invalidation proper will raise them. *) - | _ -> AD.empty () + | _ -> AD.empty () (* TODO: correct?! *) in - List.fold_right do_exp args (AD.empty ()) + List.fold_left do_exp (AD.empty ()) args in let vars = reachable @@ -164,7 +164,7 @@ struct let return_addr () = !return_addr_ let return man (exp:exp option) (f:fundec) : D.t = - let remove_var x v = List.fold_right D.remove (to_addrs v) x in + let remove_var x v = List.fold_left (Fun.flip @@ D.remove) x (to_addrs v) in let nst = List.fold_left remove_var man.local (f.slocals @ f.sformals) in match exp with | Some ret -> diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 0fb61059e2..5be4952b3c 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -55,7 +55,7 @@ struct | Queries.Regions e -> let regpart = man.global () in if is_bullet e regpart man.local then Queries.Result.bot q (* TODO: remove bot *) else - let ls = List.fold_right Queries.LS.add (regions e regpart man.local) (Queries.LS.empty ()) in + let ls = List.fold_left (Fun.flip @@ Queries.LS.add) (Queries.LS.empty ()) (regions e regpart man.local) in ls | _ -> Queries.Result.top q diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index 0850fac317..3e519d4ee3 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -43,7 +43,8 @@ struct let assign man lval rval = invalidate_lval (Analyses.ask_of_man man) lval man.local let return man exp fundec = - List.fold_right D.remove_var (fundec.sformals@fundec.slocals) man.local + let rm list acc = List.fold_left (Fun.flip @@ D.remove_var) acc list in + rm fundec.slocals (rm fundec.sformals man.local) let enter man lval f args = [(man.local,man.local)] let combine_env man lval fexp f args fc au f_ask = au diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 20d09f38d4..c01d7b314c 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -386,12 +386,12 @@ struct *) (* Give the set of reachables from argument. *) let reachables ~deep (ask: Queries.ask) es = - let reachable e st = + let reachable acc e = let q = if deep then Queries.ReachableFrom e else Queries.MayPointTo e in let ad = ask.f q in - Queries.AD.join ad st + Queries.AD.join ad acc in - List.fold_right reachable es (Queries.AD.empty ()) + List.fold_left reachable (Queries.AD.empty ()) es (* Probably ok as is. *) @@ -402,8 +402,8 @@ struct (* Just remove things that go out of scope. *) let return man exp fundec = - let rm v = remove (Analyses.ask_of_man man) (Var v,NoOffset) in - List.fold_right rm (fundec.sformals@fundec.slocals) man.local + let rm acc v = remove (Analyses.ask_of_man man) (Var v, NoOffset) acc in + List.fold_left rm man.local (fundec.sformals@fundec.slocals) (* removes all equalities with lval and then tries to make a new one: lval=rval *) let assign man (lval:lval) (rval:exp) : D.t = diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml index 467afe338b..a35e5707ea 100644 --- a/src/cdomain/value/cdomains/int/defExcDomain.ml +++ b/src/cdomain/value/cdomains/int/defExcDomain.ml @@ -299,15 +299,15 @@ struct let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in norm ik @@ (`Excluded (ex, r)) - let to_bitfield ik x = - match x with - | `Definite c -> (Z.lognot c, c) - | _ when Cil.isSigned ik -> - let one_mask = Z.lognot Z.zero in + let to_bitfield ik x = + match x with + | `Definite c -> (Z.lognot c, c) + | _ when Cil.isSigned ik -> + let one_mask = Z.lognot Z.zero in (one_mask, one_mask) - | _ -> - let one_mask = Z.lognot Z.zero in - let ik_mask = snd (Size.range ik) in + | _ -> + let one_mask = Z.lognot Z.zero in + let ik_mask = snd (Size.range ik) in (one_mask, ik_mask) let starting ?(suppress_ovwarn=false) ikind x = @@ -321,6 +321,9 @@ struct let of_excl_list t l = let r = size t in (* elements in l are excluded from the full range of t! *) `Excluded (List.fold_right S.add l (S.empty ()), r) + (* TODO: Change after #1686 has landed *) + (* `Excluded (S.of_list l, r) *) + let is_excl_list l = match l with `Excluded _ -> true | _ -> false let to_excl_list (x:t) = match x with | `Definite _ -> None @@ -542,8 +545,8 @@ struct let refine_with_congruence ik a b = a - let refine_with_bitfield ik x (z,o) = - match BitfieldDomain.Bitfield.to_int (z,o) with + let refine_with_bitfield ik x (z,o) = + match BitfieldDomain.Bitfield.to_int (z,o) with | Some y -> meet ik x (`Definite y) | _ -> diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 6643b58eef..1e70f27f1b 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1288,7 +1288,7 @@ let reset_lazy () = ResettableLazy.reset activated_library_descs let lib_funs = ref (Set.String.of_list ["__raw_read_unlock"; "__raw_write_unlock"; "spin_trylock"]) -let add_lib_funs funs = lib_funs := List.fold_right Set.String.add funs !lib_funs +let add_lib_funs funs = lib_funs := List.fold_left (Fun.flip @@ Set.String.add) !lib_funs funs let use_special fn_name = Set.String.mem fn_name !lib_funs let kernel_safe_uncalled = Set.String.of_list ["__inittest"; "init_module"; "__exittest"; "cleanup_module"]