Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 4 additions & 6 deletions src/analyses/apron/relationAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Comment thread
michael-schwarz marked this conversation as resolved.
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 =
Expand Down
6 changes: 3 additions & 3 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/analyses/malloc_null.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Comment thread
michael-schwarz marked this conversation as resolved.
match ask.f (Queries.ReachableFrom e) with
| ad when not (Queries.AD.is_top ad) ->
ad
Expand All @@ -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
Expand Down Expand Up @@ -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
Comment thread
michael-schwarz marked this conversation as resolved.
Outdated
let nst = List.fold_left remove_var man.local (f.slocals @ f.sformals) in
match exp with
| Some ret ->
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/region.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
3 changes: 2 additions & 1 deletion src/analyses/symbLocks.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions src/analyses/varEq.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand All @@ -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 =
Expand Down
23 changes: 13 additions & 10 deletions src/cdomain/value/cdomains/int/defExcDomain.ml
Comment thread
sim642 marked this conversation as resolved.
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
Expand Down Expand Up @@ -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)
| _ ->
Expand Down
2 changes: 1 addition & 1 deletion src/util/library/libraryFunctions.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down