From 6a8d71ad81dea7a830491d380593df9a6903aab7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 20 Nov 2017 03:01:04 -0800 Subject: [PATCH] [style] s/_foo/foo_/ when `foo_` is not unused Summary: Naming a variable `_foo` makes the compiler not warn about them if they are unused, but there are lots of instances of such variables in the code where they are in fact used, defeating the warning and introducing confusion for those used to this naming convention. Basically `sed -i -e "s/ _\([a-zA-Z][a-zA-Z0-9_']*\)/ \1_/g" **/*.ml` followed by manual fixing of compilation errors (lots of `compare__foo` -> `compare_foo_`). Reviewed By: mbouaziz Differential Revision: D6358837 fbshipit-source-id: 7ffb4ac --- infer/src/IR/Annot.ml | 4 +- infer/src/IR/Exp.ml | 6 +-- infer/src/IR/Localise.ml | 30 +++++------ infer/src/IR/PredSymb.ml | 14 ++--- infer/src/IR/Pvar.ml | 4 +- infer/src/IR/Sil.ml | 8 +-- infer/src/IR/Typ.ml | 2 +- infer/src/backend/BuiltinDefn.ml | 10 ++-- infer/src/backend/abs.ml | 16 +++--- infer/src/backend/buckets.ml | 4 +- infer/src/backend/dom.ml | 4 +- infer/src/backend/dotty.ml | 16 +++--- infer/src/backend/errdesc.ml | 84 ++++++++++++++--------------- infer/src/backend/paths.ml | 22 ++++---- infer/src/backend/prop.ml | 22 ++++---- infer/src/backend/propgraph.ml | 12 ++--- infer/src/backend/prover.ml | 70 ++++++++++++------------ infer/src/backend/rearrange.ml | 16 +++--- infer/src/backend/specs.ml | 8 +-- infer/src/backend/symExec.ml | 8 +-- infer/src/backend/tabulation.ml | 6 +-- infer/src/base/Config.ml | 2 +- infer/src/base/SourceFile.ml | 4 +- infer/src/checkers/accessPath.ml | 6 +-- infer/src/checkers/idenv.ml | 4 +- infer/src/clang/ComponentKit.ml | 6 +-- infer/src/clang/cFrontend_errors.ml | 10 ++-- infer/src/clang/cPredicates.ml | 26 ++++----- infer/src/clang/cTL.ml | 4 +- infer/src/clang/cTrans_utils.ml | 2 +- infer/src/concurrency/RacerD.ml | 6 +-- infer/src/eradicate/models.ml | 4 +- infer/src/eradicate/typeCheck.ml | 30 +++++------ infer/src/scripts/checkCopyright.ml | 6 +-- 34 files changed, 238 insertions(+), 238 deletions(-) diff --git a/infer/src/IR/Annot.ml b/infer/src/IR/Annot.ml index 95bd4a6cb..d75af3a5c 100644 --- a/infer/src/IR/Annot.ml +++ b/infer/src/IR/Annot.ml @@ -42,9 +42,9 @@ module Item = struct (* Don't use nonrec due to https://github.com/janestreet/ppx_compare/issues/2 *) (* type nonrec t = list (t, bool) [@@deriving compare]; *) (** Annotation for one item: a list of annotations with visibility. *) - type _t = (t * bool) list [@@deriving compare] + type t_ = (t * bool) list [@@deriving compare] - type t = _t [@@deriving compare] + type t = t_ [@@deriving compare] let equal = [%compare.equal : t] diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index 9e73c62f4..45cdc0db4 100644 --- a/infer/src/IR/Exp.ml +++ b/infer/src/IR/Exp.ml @@ -16,9 +16,9 @@ module L = Logging module F = Format (* reverse the natural order on Var *) -type _ident = Ident.t +type ident_ = Ident.t -let compare__ident x y = Ident.compare y x +let compare_ident_ x y = Ident.compare y x type closure = {name: Typ.Procname.t; captured_vars: (t * Pvar.t * Typ.t) list} @@ -36,7 +36,7 @@ and sizeof_data = {typ: Typ.t; nbytes: int option; dynamic_length: t option; sub (** Program expressions. *) and t = - | Var of _ident (** Pure variable: it is not an lvalue *) + | Var of ident_ (** Pure variable: it is not an lvalue *) | UnOp of Unop.t * t * Typ.t option (** Unary operator with type of the result if known *) | BinOp of Binop.t * t * t (** Binary operator *) | Exn of t (** Exception *) diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 4fe520e5c..2cf0b2f60 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -217,7 +217,7 @@ let error_desc_equal desc1 desc2 = [%compare.equal : string list] (desc_get_comparable desc1) (desc_get_comparable desc2) -let _line_tag tags tag loc = +let line_tag_ tags tag loc = let line_str = string_of_int loc.Location.line in Tags.update tags tag line_str ; let s = "line " ^ line_str in @@ -227,9 +227,9 @@ let _line_tag tags tag loc = else s -let at_line_tag tags tag loc = "at " ^ _line_tag tags tag loc +let at_line_tag tags tag loc = "at " ^ line_tag_ tags tag loc -let _line tags loc = _line_tag tags Tags.line loc +let line_ tags loc = line_tag_ tags Tags.line loc let at_line tags loc = at_line_tag tags Tags.line loc @@ -295,20 +295,20 @@ type deref_str = let pointer_or_object () = if Config.curr_language_is Config.Java then "object" else "pointer" -let _deref_str_null proc_name_opt _problem_str tags = - let problem_str = add_by_call_to_opt _problem_str tags proc_name_opt in +let deref_str_null_ proc_name_opt problem_str_ tags = + let problem_str = add_by_call_to_opt problem_str_ tags proc_name_opt in {tags; value_pre= Some (pointer_or_object ()); value_post= None; problem_str} (** dereference strings for null dereference *) let deref_str_null proc_name_opt = let problem_str = "could be null and is dereferenced" in - _deref_str_null proc_name_opt problem_str (Tags.create ()) + deref_str_null_ proc_name_opt problem_str (Tags.create ()) let access_str_empty proc_name_opt = let problem_str = "could be empty and is accessed" in - _deref_str_null proc_name_opt problem_str (Tags.create ()) + deref_str_null_ proc_name_opt problem_str (Tags.create ()) (** dereference strings for null dereference due to Nullable annotation *) @@ -317,7 +317,7 @@ let deref_str_nullable proc_name_opt nullable_obj_str = Tags.update tags Tags.nullable_src nullable_obj_str ; (* to be completed once we know if the deref'd expression is directly or transitively @Nullable*) let problem_str = "" in - _deref_str_null proc_name_opt problem_str tags + deref_str_null_ proc_name_opt problem_str tags (** dereference strings for null dereference due to weak captured variable in block *) @@ -325,7 +325,7 @@ let deref_str_weak_variable_in_block proc_name_opt nullable_obj_str = let tags = Tags.create () in Tags.update tags Tags.weak_captured_var_src nullable_obj_str ; let problem_str = "" in - _deref_str_null proc_name_opt problem_str tags + deref_str_null_ proc_name_opt problem_str tags (** dereference strings for nonterminal nil arguments in c/objc variadic methods *) @@ -341,7 +341,7 @@ let deref_str_nil_argument_in_variadic_method pn total_args arg_number = (Typ.Procname.to_simplified_string pn) arg_number (total_args - 1) nil_null function_method in - _deref_str_null None problem_str tags + deref_str_null_ None problem_str tags (** dereference strings for an undefined value coming from the given procedure *) @@ -800,7 +800,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc match bucket_opt with Some bucket -> Tags.update tags Tags.bucket bucket | None -> () in let xxx_allocated_to = - let value_str, _to, _on = + let value_str, to_, on_ = match value_str_opt with | None -> ("", "", "") @@ -817,11 +817,11 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc let desc_str = match resource_opt with | Some PredSymb.Rmemory _ -> - mem_dyn_allocated ^ _to ^ value_str + mem_dyn_allocated ^ to_ ^ value_str | Some PredSymb.Rfile -> - "resource" ^ typ_str ^ "acquired" ^ _to ^ value_str + "resource" ^ typ_str ^ "acquired" ^ to_ ^ value_str | Some PredSymb.Rlock -> - lock_acquired ^ _on ^ value_str + lock_acquired ^ on_ ^ value_str | Some PredSymb.Rignore | None -> if is_none value_str_opt then "memory" else value_str in @@ -840,7 +840,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc | Some PredSymb.Rignore | None -> reachable in - ["is not " ^ rxxx ^ " after " ^ _line tags loc] + ["is not " ^ rxxx ^ " after " ^ line_ tags loc] in let bucket_str = match bucket_opt with Some bucket when Config.show_buckets -> bucket | _ -> "" diff --git a/infer/src/IR/PredSymb.ml b/infer/src/IR/PredSymb.ml index 5056e0f64..0fba8d2b8 100644 --- a/infer/src/IR/PredSymb.ml +++ b/infer/src/IR/PredSymb.ml @@ -75,17 +75,17 @@ let compare_res_action {ra_kind= k1; ra_res= r1} {ra_kind= k2; ra_res= r2} = (* type aliases for components of t values that compare should ignore *) -type _annot_item = Annot.Item.t +type annot_item_ = Annot.Item.t -let compare__annot_item _ _ = 0 +let compare_annot_item_ _ _ = 0 -type _location = Location.t +type location_ = Location.t -let compare__location _ _ = 0 +let compare_location_ _ _ = 0 -type _path_pos = path_pos +type path_pos_ = path_pos -let compare__path_pos _ _ = 0 +let compare_path_pos_ _ _ = 0 (** Attributes are nary function symbols that are applied to expression arguments in Apred and Anpred atomic formulas. Many operations don't make much sense for nullary predicates, and are @@ -99,7 +99,7 @@ type t = | Aresource of res_action (** resource acquire/release *) | Aautorelease | Adangling of dangling_kind (** dangling pointer *) - | Aundef of Typ.Procname.t * _annot_item * _location * _path_pos + | Aundef of Typ.Procname.t * annot_item_ * location_ * path_pos_ | Alocked | Aunlocked | Adiv0 of path_pos (** value appeared in second argument of division at given path position *) diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index c1d2b873b..c99ae2109 100644 --- a/infer/src/IR/Pvar.ml +++ b/infer/src/IR/Pvar.ml @@ -62,7 +62,7 @@ let pp_translation_unit fmt = function Format.fprintf fmt "EXTERN" -let _pp f pv = +let pp_ f pv = let name = pv.pv_name in match pv.pv_kind with | Local_var n -> @@ -110,7 +110,7 @@ let pp_latex f pv = (** Pretty print a pvar which denotes a value, not an address *) let pp_value pe f pv = - match pe.Pp.kind with TEXT -> _pp f pv | HTML -> _pp f pv | LATEX -> pp_latex f pv + match pe.Pp.kind with TEXT -> pp_ f pv | HTML -> pp_ f pv | LATEX -> pp_latex f pv (** Pretty print a program variable. *) diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 00c1ddab3..36e359900 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -1958,7 +1958,7 @@ let rec sexp_compact sh se = (** Return a compact representation of the hpred *) -let _hpred_compact sh hpred = +let hpred_compact_ sh hpred = match hpred with | Hpointsto (e1, se, e2) -> let e1' = exp_compact sh e1 in @@ -1973,7 +1973,7 @@ let _hpred_compact sh hpred = let hpred_compact sh hpred = try HpredInstHash.find sh.hpredh hpred with Not_found -> - let hpred' = _hpred_compact sh hpred in + let hpred' = hpred_compact_ sh hpred in HpredInstHash.add sh.hpredh hpred' hpred' ; hpred' @@ -2043,7 +2043,7 @@ let sigma_to_sigma_ne sigma : (atom list * hpred list) list = (** [hpara_instantiate para e1 e2 elist] instantiates [para] with [e1], [e2] and [elist]. If [para = lambda (x, y, xs). exists zs. b], - then the result of the instantiation is [b\[e1 / x, e2 / y, elist / xs, _zs'/ zs\]] + then the result of the instantiation is [b\[e1 / x, e2 / y, elist / xs, zs'_/ zs\]] for some fresh [_zs'].*) let hpara_instantiate para e1 e2 elist = let subst_for_svars = @@ -2068,7 +2068,7 @@ let hpara_instantiate para e1 e2 elist = (** [hpara_dll_instantiate para cell blink flink elist] instantiates [para] with [cell], [blink], [flink], and [elist]. If [para = lambda (x, y, z, xs). exists zs. b], then the result of the instantiation is - [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]] + [b\[cell / x, blink / y, flink / z, elist / xs, zs'_/ zs\]] for some fresh [_zs'].*) let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist = let subst_for_svars = diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 84c347ce9..196864ba7 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -28,7 +28,7 @@ type ikind = | ILong (** [long] *) | IULong (** [unsigned long] *) | ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *) - | IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft Visual C) *) + | IULongLong (** [unsigned long long] (or [unsigned int64_] on Microsoft Visual C) *) | I128 (** [__int128_t] *) | IU128 (** [__uint128_t] *) [@@deriving compare] diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index d237a5203..0ef8b8d65 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -619,7 +619,7 @@ let execute_abort {Builtin.proc_name} : Builtin.ret_typ = let execute_exit {Builtin.prop_; path} : Builtin.ret_typ = SymExec.diverge prop_ path -let _execute_free tenv mk loc acc iter = +let execute_free_ tenv mk loc acc iter = match Prop.prop_iter_current tenv iter with | Sil.Hpointsto (lexp, _, _), [] -> let prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in @@ -645,7 +645,7 @@ let _execute_free tenv mk loc acc iter = (* should not happen *) -let _execute_free_nonzero mk pdesc tenv instr prop lexp typ loc = +let execute_free_nonzero_ mk pdesc tenv instr prop lexp typ loc = try match Prover.is_root tenv prop lexp lexp with | None -> @@ -653,7 +653,7 @@ let _execute_free_nonzero mk pdesc tenv instr prop lexp typ loc = assert false | Some _ -> let prop_list = - List.fold ~f:(_execute_free tenv mk loc) ~init:[] + List.fold ~f:(execute_free_ tenv mk loc) ~init:[] (Rearrange.rearrange pdesc tenv lexp typ prop loc) in List.rev prop_list @@ -685,10 +685,10 @@ let execute_free mk {Builtin.pdesc; instr; tenv; prop_; path; args; loc} : Built in let plist = prop_zero - @ (* model: if 0 then skip else _execute_free_nonzero *) + @ (* model: if 0 then skip else execute_free_nonzero_ *) List.concat_map ~f:(fun p -> - _execute_free_nonzero mk pdesc tenv instr p + execute_free_nonzero_ mk pdesc tenv instr p (Prop.exp_normalize_prop tenv p lexp) typ loc) prop_nonzero diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index ff91369a2..f5aac8e5d 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1079,12 +1079,12 @@ let should_raise_objc_leak hpred = None -let get_retain_cycle_dotty _prop cycle = - match _prop with +let get_retain_cycle_dotty prop_ cycle = + match prop_ with | None -> None - | Some Some _prop -> - Dotty.dotty_prop_to_str _prop cycle + | Some Some prop_ -> + Dotty.dotty_prop_to_str prop_ cycle | _ -> None @@ -1140,7 +1140,7 @@ let get_var_retain_cycle prop_ = do_sigma sigma -let remove_opt _prop = match _prop with Some Some p -> p | _ -> Prop.prop_emp +let remove_opt prop_ = match prop_ with Some Some p -> p | _ -> Prop.prop_emp (** Checks if cycle has fields (derived from a property or directly defined as ivar) with attributes weak/unsafe_unretained/assing *) @@ -1514,16 +1514,16 @@ let abstract_footprint pname (tenv: Tenv.t) (prop: Prop.normal Prop.t) : Prop.no Prop.normalize tenv prop' -let _abstract pname pay tenv p = +let abstract_ pname pay tenv p = if pay then SymOp.pay () ; (* pay one symop *) let p' = if !Config.footprint then abstract_footprint pname tenv p else p in abstract_prop pname tenv ~rename_primed:true ~from_abstract_footprint:false p' -let abstract pname tenv p = _abstract pname true tenv p +let abstract pname tenv p = abstract_ pname true tenv p -let abstract_no_symop pname tenv p = _abstract pname false tenv p +let abstract_no_symop pname tenv p = abstract_ pname false tenv p let lifted_abstract pname tenv pset = let f p = if Prover.check_inconsistency tenv p then None else Some (abstract pname tenv p) in diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index af32de598..0d0166d0b 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -44,8 +44,8 @@ let check_nested_loop path pos_opt = let do_any_node _level _node = incr trace_length (* L.d_strln *) - (* ("level " ^ string_of_int _level ^ *) - (* " (Procdesc.Node.get_id node) " ^ string_of_int (Procdesc.Node.get_id _node)) *) + (* ("level " ^ string_of_int level_ ^ *) + (* " (Procdesc.Node.get_id node) " ^ string_of_int (Procdesc.Node.get_id node_)) *) in let f level p _ _ = match Paths.Path.curr_node p with diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 649db5ec0..584d62f03 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -2164,9 +2164,9 @@ let pathset_join pname tenv (pset1: Paths.PathSet.t) (pset2: Paths.PathSet.t) let ppa2_new, ppalist1_cur' = join_proppath_plist [] ppa2'' ppalist1_cur in join ppalist1_cur' (ppa2_new :: ppalist2_acc') ppalist2_rest' in - let _ppalist1_res, _ppalist2_res = join ppalist1 [] ppalist2 in + let ppalist1_res_, ppalist2_res_ = join ppalist1 [] ppalist2 in let ren l = List.map ~f:(fun (p, x) -> (Prop.prop_rename_primed_footprint_vars tenv p, x)) l in - let ppalist1_res, ppalist2_res = (ren _ppalist1_res, ren _ppalist2_res) in + let ppalist1_res, ppalist2_res = (ren ppalist1_res_, ren ppalist2_res_) in let res = (Paths.PathSet.from_renamed_list ppalist1_res, Paths.PathSet.from_renamed_list ppalist2_res) in diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 7aa6aa394..a5413f4e4 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -1003,25 +1003,25 @@ and display_pure_info f pe prop = (** Pretty print a proposition in dotty format. *) -and pp_dotty f kind (_prop: Prop.normal Prop.t) cycle = +and pp_dotty f kind (prop_: Prop.normal Prop.t) cycle = incr proposition_counter ; let pe, prop = match kind with | Spec_postcondition pre -> target_invisible_arrow_pre := !proposition_counter ; let diff = - Propgraph.compute_diff Black (Propgraph.from_prop pre) (Propgraph.from_prop _prop) + Propgraph.compute_diff Black (Propgraph.from_prop pre) (Propgraph.from_prop prop_) in let cmap_norm = Propgraph.diff_get_colormap false diff in let cmap_foot = Propgraph.diff_get_colormap true diff in let pe = {(Prop.prop_update_obj_sub Pp.text pre) with cmap_norm; cmap_foot} in (* add stack vars from pre *) let pre_stack = fst (Prop.sigma_get_stack_nonstack true pre.Prop.sigma) in - let prop = Prop.set _prop ~sigma:(pre_stack @ _prop.Prop.sigma) in + let prop = Prop.set prop_ ~sigma:(pre_stack @ prop_.Prop.sigma) in (pe, Prop.normalize (Tenv.create ()) prop) | _ -> - let pe = Prop.prop_update_obj_sub Pp.text _prop in - (pe, _prop) + let pe = Prop.prop_update_obj_sub Pp.text prop_ in + (pe, prop_) in dangling_dotboxes := [] ; nil_dotboxes := [] ; @@ -1681,11 +1681,11 @@ let reset_node_counter () = global_node_counter := 0 let print_specs_xml signature specs loc fmt = reset_node_counter () ; let do_one_spec pre posts n = - let add_stack_to_prop _prop = + let add_stack_to_prop prop_ = (* add stack vars from pre *) let pre_stack = fst (Prop.sigma_get_stack_nonstack true pre.Prop.sigma) in - let _prop' = Prop.set _prop ~sigma:(pre_stack @ _prop.Prop.sigma) in - Prop.normalize (Tenv.create ()) _prop' + let prop'_ = Prop.set prop_ ~sigma:(pre_stack @ prop_.Prop.sigma) in + Prop.normalize (Tenv.create ()) prop'_ in let jj = ref 0 in let xml_pre = prop_to_xml pre "precondition" !jj in diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 50228edd9..2d41cff1e 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -188,7 +188,7 @@ let find_normal_variable_funcall (node: Procdesc.Node.t) (id: Ident.t) (** Find a program variable assignment in the current node or predecessors. *) let find_program_variable_assignment node pvar : (Procdesc.Node.t * Ident.t) option = let find_instr node = function - | Sil.Store (Exp.Lvar _pvar, _, Exp.Var id, _) when Pvar.equal pvar _pvar && Ident.is_normal id -> + | Sil.Store (Exp.Lvar pvar_, _, Exp.Var id, _) when Pvar.equal pvar pvar_ && Ident.is_normal id -> Some (node, id) | _ -> None @@ -219,7 +219,7 @@ let find_struct_by_value_assignment node pvar = (** Find a program variable assignment to id in the current node or predecessors. *) let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option = let find_instr node = function - | Sil.Load (_id, e, _, _) when Ident.equal _id id -> + | Sil.Load (id_, e, _, _) when Ident.equal id_ id -> Some (node, e) | _ -> None @@ -232,7 +232,7 @@ let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option = let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = let find_instr n = let filter = function - | Sil.Store (Exp.Lvar _pvar, _, Exp.Const Const.Cint i, _) when Pvar.equal pvar _pvar -> + | Sil.Store (Exp.Lvar pvar_, _, Exp.Const Const.Cint i, _) when Pvar.equal pvar pvar_ -> IntLit.iszero i <> true_branch | _ -> false @@ -250,21 +250,21 @@ let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = (** Find the Load instruction used to declare normal variable [id], and return the expression dereferenced to initialize [id] *) -let rec _find_normal_variable_load tenv (seen: Exp.Set.t) node id : DExp.t option = +let rec find_normal_variable_load_ tenv (seen: Exp.Set.t) node id : DExp.t option = let find_declaration node = function | Sil.Load (id0, e, _, _) when Ident.equal id id0 -> if verbose then ( L.d_str "find_normal_variable_load defining " ; Sil.d_exp e ; L.d_ln () ) ; - _exp_lv_dexp tenv seen node e + exp_lv_dexp_ tenv seen node e | Sil.Call (Some (id0, _), Exp.Const Const.Cfun pn, (e, _) :: _, _, _) when Ident.equal id id0 && Typ.Procname.equal pn (Typ.Procname.from_string_c_fun "__cast") -> if verbose then ( L.d_str "find_normal_variable_load cast on " ; Sil.d_exp e ; L.d_ln () ) ; - _exp_rv_dexp tenv seen node e + exp_rv_dexp_ tenv seen node e | Sil.Call (Some (id0, _), (Exp.Const Const.Cfun pname as fun_exp), args, loc, call_flags) when Ident.equal id id0 -> if verbose then ( @@ -273,7 +273,7 @@ let rec _find_normal_variable_load tenv (seen: Exp.Set.t) node id : DExp.t optio L.d_ln () ) ; let fun_dexp = DExp.Dconst (Const.Cfun pname) in let args_dexp = - let args_dexpo = List.map ~f:(fun (e, _) -> _exp_rv_dexp tenv seen node e) args in + let args_dexpo = List.map ~f:(fun (e, _) -> exp_rv_dexp_ tenv seen node e) args in if List.exists ~f:is_none args_dexpo then [] else let unNone = function Some x -> x | None -> assert false in @@ -301,14 +301,14 @@ let rec _find_normal_variable_load tenv (seen: Exp.Set.t) node id : DExp.t optio (** describe lvalue [e] as a dexp *) -and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = - if Exp.Set.mem e _seen then ( +and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option = + if Exp.Set.mem e seen_ then ( L.d_str "exp_lv_dexp: cycle detected" ; Sil.d_exp e ; L.d_ln () ; None ) else - let seen = Exp.Set.add e _seen in + let seen = Exp.Set.add e seen_ in match Prop.exp_normalize_noabs tenv Sil.sub_empty e with | Exp.Const c -> if verbose then ( L.d_str "exp_lv_dexp: constant " ; Sil.d_exp e ; L.d_ln () ) ; @@ -319,7 +319,7 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = L.d_str "exp_lv_dexp: (e1 +PI e2) " ; Sil.d_exp e ; L.d_ln () ) ; - match (_exp_lv_dexp tenv seen node e1, _exp_rv_dexp tenv seen node e2) with + match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | Some de1, Some de2 -> Some (DExp.Dbinop (Binop.PlusPI, de1, de2)) | _ -> @@ -330,7 +330,7 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = L.d_str "exp_lv_dexp: normal var " ; Sil.d_exp e ; L.d_ln () ) ; - match _find_normal_variable_load tenv seen node id with + match find_normal_variable_load_ tenv seen node id with | None -> None | Some de -> @@ -351,15 +351,15 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = | Some (node', id) -> match find_normal_variable_funcall node' id with | Some (fun_exp, eargs, loc, call_flags) -> - let fun_dexpo = _exp_rv_dexp tenv seen node' fun_exp in - let blame_args = List.map ~f:(_exp_rv_dexp tenv seen node') eargs in + let fun_dexpo = exp_rv_dexp_ tenv seen node' fun_exp in + let blame_args = List.map ~f:(exp_rv_dexp_ tenv seen node') eargs in if List.exists ~f:is_none (fun_dexpo :: blame_args) then None else let unNone = function Some x -> x | None -> assert false in let args = List.map ~f:unNone blame_args in Some (DExp.Dfcall (unNone fun_dexpo, args, loc, call_flags)) | None -> - _exp_rv_dexp tenv seen node' (Exp.Var id) + exp_rv_dexp_ tenv seen node' (Exp.Var id) else Some (DExp.Dpvar pvar) | Exp.Lfield (Exp.Var id, f, _) when Ident.is_normal id -> ( @@ -368,7 +368,7 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = Sil.d_exp (Exp.Var id) ; L.d_str (" " ^ Typ.Fieldname.to_string f) ; L.d_ln () ) ; - match _find_normal_variable_load tenv seen node id with + match find_normal_variable_load_ tenv seen node id with | None -> None | Some de -> @@ -380,7 +380,7 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = Sil.d_exp e1 ; L.d_str (" " ^ Typ.Fieldname.to_string f) ; L.d_ln () ) ; - match _exp_lv_dexp tenv seen node e1 with + match exp_lv_dexp_ tenv seen node e1 with | None -> None | Some de -> @@ -389,7 +389,7 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = -> ( if verbose then ( L.d_str "exp_lv_dexp: Lindex " ; Sil.d_exp e1 ; L.d_str " " ; Sil.d_exp e2 ; L.d_ln () ) ; - match (_exp_lv_dexp tenv seen node e1, _exp_rv_dexp tenv seen node e2) with + match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | None, _ -> None | Some de1, None -> @@ -406,14 +406,14 @@ and _exp_lv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = (** describe rvalue [e] as a dexp *) -and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = - if Exp.Set.mem e _seen then ( +and exp_rv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option = + if Exp.Set.mem e seen_ then ( L.d_str "exp_rv_dexp: cycle detected" ; Sil.d_exp e ; L.d_ln () ; None ) else - let seen = Exp.Set.add e _seen in + let seen = Exp.Set.add e seen_ in match e with | Exp.Const c -> if verbose then ( L.d_str "exp_rv_dexp: constant " ; Sil.d_exp e ; L.d_ln () ) ; @@ -424,14 +424,14 @@ and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = Sil.d_exp e ; L.d_ln () ) ; if Pvar.is_frontend_tmp pv then - _exp_lv_dexp tenv _seen (* avoid spurious cycle detection *) node e + exp_lv_dexp_ tenv seen_ (* avoid spurious cycle detection *) node e else Some (DExp.Dpvaraddr pv) | Exp.Var id when Ident.is_normal id -> if verbose then ( L.d_str "exp_rv_dexp: normal var " ; Sil.d_exp e ; L.d_ln () ) ; - _find_normal_variable_load tenv seen node id + find_normal_variable_load_ tenv seen node id | Exp.Lfield (e1, f, _) -> ( if verbose then ( @@ -439,7 +439,7 @@ and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = Sil.d_exp e1 ; L.d_str (" " ^ Typ.Fieldname.to_string f) ; L.d_ln () ) ; - match _exp_rv_dexp tenv seen node e1 with + match exp_rv_dexp_ tenv seen node e1 with | None -> None | Some de -> @@ -448,7 +448,7 @@ and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = -> ( if verbose then ( L.d_str "exp_rv_dexp: Lindex " ; Sil.d_exp e1 ; L.d_str " " ; Sil.d_exp e2 ; L.d_ln () ) ; - match (_exp_rv_dexp tenv seen node e1, _exp_rv_dexp tenv seen node e2) with + match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | None, _ | _, None -> None | Some de1, Some de2 -> @@ -456,7 +456,7 @@ and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = | Exp.BinOp (op, e1, e2) -> ( if verbose then ( L.d_str "exp_rv_dexp: BinOp " ; Sil.d_exp e ; L.d_ln () ) ; - match (_exp_rv_dexp tenv seen node e1, _exp_rv_dexp tenv seen node e2) with + match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | None, _ | _, None -> None | Some de1, Some de2 -> @@ -464,18 +464,18 @@ and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = | Exp.UnOp (op, e1, _) -> ( if verbose then ( L.d_str "exp_rv_dexp: UnOp " ; Sil.d_exp e ; L.d_ln () ) ; - match _exp_rv_dexp tenv seen node e1 with + match exp_rv_dexp_ tenv seen node e1 with | None -> None | Some de1 -> Some (DExp.Dunop (op, de1)) ) | Exp.Cast (_, e1) -> if verbose then ( L.d_str "exp_rv_dexp: Cast " ; Sil.d_exp e ; L.d_ln () ) ; - _exp_rv_dexp tenv seen node e1 + exp_rv_dexp_ tenv seen node e1 | Exp.Sizeof {typ; dynamic_length; subtype} -> if verbose then ( L.d_str "exp_rv_dexp: type " ; Sil.d_exp e ; L.d_ln () ) ; Some - (DExp.Dsizeof (typ, Option.bind dynamic_length ~f:(_exp_rv_dexp tenv seen node), subtype)) + (DExp.Dsizeof (typ, Option.bind dynamic_length ~f:(exp_rv_dexp_ tenv seen node), subtype)) | _ -> if verbose then ( L.d_str "exp_rv_dexp: no match for " ; @@ -484,11 +484,11 @@ and _exp_rv_dexp tenv (_seen: Exp.Set.t) node e : DExp.t option = None -let find_normal_variable_load tenv = _find_normal_variable_load tenv Exp.Set.empty +let find_normal_variable_load tenv = find_normal_variable_load_ tenv Exp.Set.empty -let exp_lv_dexp tenv = _exp_lv_dexp tenv Exp.Set.empty +let exp_lv_dexp tenv = exp_lv_dexp_ tenv Exp.Set.empty -let exp_rv_dexp tenv = _exp_rv_dexp tenv Exp.Set.empty +let exp_rv_dexp tenv = exp_rv_dexp_ tenv Exp.Set.empty (** Produce a description of a mismatch between an allocation function and a deallocation function *) @@ -676,8 +676,8 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (** find the dexp, if any, where the given value is stored also return the type of the value if found *) -let vpath_find tenv prop _exp : DExp.t option * Typ.t option = - if verbose then ( L.d_str "in vpath_find exp:" ; Sil.d_exp _exp ; L.d_ln () ) ; +let vpath_find tenv prop exp_ : DExp.t option * Typ.t option = + if verbose then ( L.d_str "in vpath_find exp:" ; Sil.d_exp exp_ ; L.d_ln () ) ; let rec find sigma_acc sigma_todo exp = let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with @@ -771,12 +771,12 @@ let vpath_find tenv prop _exp : DExp.t option * Typ.t option = | None, _ -> find (hpred :: sigma_acc) sigma_todo' exp in - let res = find [] prop.Prop.sigma _exp in + let res = find [] prop.Prop.sigma exp_ in ( if verbose then match res with | None, _ -> L.d_str "vpath_find: cannot find " ; - Sil.d_exp _exp ; + Sil.d_exp exp_ ; L.d_ln () | Some de, typo -> L.d_str "vpath_find: found " ; @@ -928,7 +928,7 @@ let explain_dexp_access prop dexp is_nullable = access_opt -let explain_dereference_access outermost_array is_nullable _de_opt prop = +let explain_dereference_access outermost_array is_nullable de_opt_ prop = let de_opt = let rec remove_outermost_array_access = function (* remove outermost array access from [de] *) @@ -950,7 +950,7 @@ let explain_dereference_access outermost_array is_nullable _de_opt prop = | de -> de in - match _de_opt with + match de_opt_ with | None -> None | Some de -> @@ -1008,7 +1008,7 @@ let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_arr if outermost_array is true, the outermost array access is removed if outermost_dereference is true, stop at the outermost dereference (skipping e.g. outermost field access) *) -let _explain_access proc_name tenv ?(use_buckets= false) ?(outermost_array= false) +let explain_access_ proc_name tenv ?(use_buckets= false) ?(outermost_array= false) ?(outermost_dereference= false) ?(is_nullable= false) ?(is_premature_nil= false) deref_str prop loc = let rec find_outermost_dereference node e = @@ -1113,18 +1113,18 @@ let _explain_access proc_name tenv ?(use_buckets= false) ?(outermost_array= fals The subexpression to focus on is obtained by removing field and index accesses. *) let explain_dereference proc_name tenv ?(use_buckets= false) ?(is_nullable= false) ?(is_premature_nil= false) deref_str prop loc = - _explain_access proc_name tenv ~use_buckets ~outermost_array:false ~outermost_dereference:true + explain_access_ proc_name tenv ~use_buckets ~outermost_array:false ~outermost_dereference:true ~is_nullable ~is_premature_nil deref_str prop loc (** Produce a description of the array access performed in the current instruction, if any. The subexpression to focus on is obtained by removing the outermost array access. *) let explain_array_access tenv deref_str prop loc = - _explain_access tenv ~outermost_array:true deref_str prop loc + explain_access_ tenv ~outermost_array:true deref_str prop loc (** Produce a description of the memory access performed in the current instruction, if any. *) -let explain_memory_access tenv deref_str prop loc = _explain_access tenv deref_str prop loc +let explain_memory_access tenv deref_str prop loc = explain_access_ tenv deref_str prop loc (* offset of an expression found following a program variable *) type pvar_off = diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 4731c2675..0e77b520c 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -86,31 +86,31 @@ end = struct (* number of linear sequences described by the path *) } (* type aliases for components of t values that compare should ignore *) - type _stats = stats + type stats_ = stats - let compare__stats _ _ = 0 + let compare_stats_ _ _ = 0 - type _procname = Typ.Procname.t + type procname_ = Typ.Procname.t - let compare__procname _ _ = 0 + let compare_procname_ _ _ = 0 - type _string_option = string option + type string_option_ = string option - let compare__string_option _ _ = 0 + let compare_string_option_ _ _ = 0 - type _path_exec = + type path_exec_ = | ExecSkipped of string * Location.t option (** call was skipped with a reason *) | ExecCompleted of t (** call was completed *) and t = (* INVARIANT: stats are always set to dummy_stats unless we are in the middle of a traversal *) (* in particular: a new traversal cannot be initiated during an existing traversal *) - | Pstart of Procdesc.Node.t * _stats (** start node *) - | Pnode of Procdesc.Node.t * Typ.Name.t option * session * t * _stats * _string_option + | Pstart of Procdesc.Node.t * stats_ (** start node *) + | Pnode of Procdesc.Node.t * Typ.Name.t option * session * t * stats_ * string_option_ (** we got to [node] from last [session] perhaps propagating exception [exn_opt], and continue with [path]. *) - | Pjoin of t * t * _stats (** join of two paths *) - | Pcall of t * _procname * _path_exec * _stats (** add a sub-path originating from a call *) + | Pjoin of t * t * stats_ (** join of two paths *) + | Pcall of t * procname_ * path_exec_ * stats_ (** add a sub-path originating from a call *) [@@deriving compare] let get_dummy_stats () = {max_length= -1; linear_num= -1.0} diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index bdc60d3b3..398e2f7e7 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -101,8 +101,8 @@ let equal_prop p1 p2 = Int.equal (compare_prop p1 p2) 0 (** {1 Functions for Pretty Printing} *) (** Pretty print a footprint. *) -let pp_footprint _pe f fp = - let pe = {_pe with Pp.cmap_norm= _pe.Pp.cmap_foot} in +let pp_footprint pe_ f fp = + let pe = {pe_ with Pp.cmap_norm= pe_.Pp.cmap_foot} in let pp_pi f () = if fp.pi_fp <> [] then F.fprintf f "%a ;@\n" @@ -199,8 +199,8 @@ let sigma_get_stack_nonstack only_local_vars sigma = (** Pretty print a sigma in simple mode. *) let pp_sigma_simple pe env fmt sigma = let sigma_stack, sigma_nonstack = sigma_get_stack_nonstack false sigma in - let pp_stack fmt _sg = - let sg = List.sort ~cmp:Sil.compare_hpred _sg in + let pp_stack fmt sg_ = + let sg = List.sort ~cmp:Sil.compare_hpred sg_ in if sg <> [] then Format.fprintf fmt "%a" (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) sg in @@ -270,8 +270,8 @@ let pp_evars pe f evars = (** Print an hpara in simple mode *) -let pp_hpara_simple _pe env n f pred = - let pe = Pp.reset_obj_sub _pe in +let pp_hpara_simple pe_ env n f pred = + let pe = Pp.reset_obj_sub pe_ in (* no free vars: disable object substitution *) match pe.kind with | TEXT | HTML -> @@ -285,8 +285,8 @@ let pp_hpara_simple _pe env n f pred = (** Print an hpara_dll in simple mode *) -let pp_hpara_dll_simple _pe env n f pred = - let pe = Pp.reset_obj_sub _pe in +let pp_hpara_dll_simple pe_ env n f pred = + let pe = Pp.reset_obj_sub pe_ in (* no free vars: disable object substitution *) match pe.kind with | TEXT | HTML -> @@ -322,8 +322,8 @@ let prop_update_obj_sub pe prop = (** Pretty print a footprint in simple mode. *) -let pp_footprint_simple _pe env f fp = - let pe = {_pe with Pp.cmap_norm= _pe.Pp.cmap_foot} in +let pp_footprint_simple pe_ env f fp = + let pe = {pe_ with Pp.cmap_norm= pe_.Pp.cmap_foot} in let pp_pure f pi = if pi <> [] then F.fprintf f "%a *@\n" (pp_pi pe) pi in if fp.pi_fp <> [] || fp.sigma_fp <> [] then F.fprintf f "@\n[footprint@\n @[%a%a@] ]" pp_pure fp.pi_fp (pp_sigma_simple pe env) @@ -2301,7 +2301,7 @@ let exist_quantify tenv fav (prop: normal t) : normal t = let gen_fresh_id_sub id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in let ren_sub = Sil.exp_subst_of_list (List.map ~f:gen_fresh_id_sub ids) in let prop' = - (* throw away x=E if x becomes _x *) + (* throw away x=E if x becomes x_ *) let mem_idlist i = List.exists ~f:(fun id -> Ident.equal i id) in let sub = Sil.sub_filter (fun i -> not (mem_idlist i ids)) prop.sub in if Sil.equal_exp_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub) diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 93d9bd186..1d8c71ab2 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -279,10 +279,10 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = let rec pp_seq_newline n f = function | [] -> () - | [_x] + | [x_] -> ( - let pe = update_pe_diff _x in - let x = add_base_stack _x in + let pe = update_pe_diff x_ in + let x = add_base_stack x_ in match pe.kind with | TEXT -> F.fprintf f "%s %d of %d:@\n%a" s n num (Prop.pp_prop pe) x @@ -290,9 +290,9 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = F.fprintf f "%s %d of %d:@\n%a@\n" s n num (Prop.pp_prop pe) x | LATEX -> F.fprintf f "@[%a@]@\n" (Prop.pp_prop pe) x ) - | _x :: l -> - let pe = update_pe_diff _x in - let x = add_base_stack _x in + | x_ :: l -> + let pe = update_pe_diff x_ in + let x = add_base_stack x_ in match pe.kind with | TEXT -> F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 3a058bdd0..808f683bb 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -174,7 +174,7 @@ end = struct else combine acc_todos (constr' :: acc_seen) constraints_new rest' - let rec _saturate seen todos = + let rec saturate_ seen todos = (* seen is a superset of todos. "seen" is sorted and doesn't have redundancy. *) match todos with | [] -> @@ -188,12 +188,12 @@ end = struct (* Important to use queue here. Otherwise, might diverge *) let rest_new = remove_redundancy (rest @ todos_new) in let seen_new' = sort_then_remove_redundancy seen_new in - _saturate seen_new' rest_new + saturate_ seen_new' rest_new let saturate constraints = let constraints_cleaned = sort_then_remove_redundancy constraints in - _saturate constraints_cleaned constraints_cleaned + saturate_ constraints_cleaned constraints_cleaned end @@ -551,8 +551,8 @@ end = struct (** Check [prop |- e1!=e2]. Result [false] means "don't know". *) - let check_ne ineq _e1 _e2 = - let e1, e2 = if Exp.compare _e1 _e2 <= 0 then (_e1, _e2) else (_e2, _e1) in + let check_ne ineq e1_ e2_ = + let e1, e2 = if Exp.compare e1_ e2_ <= 0 then (e1_, e2_) else (e2_, e1_) in List.exists ~f:(exp_pair_eq (e1, e2)) ineq.neqs || check_lt ineq e1 e2 || check_lt ineq e2 e1 @@ -1221,7 +1221,7 @@ end = struct let get_missing_typ () = !missing_typ - let _d_missing sub = + let d_missing_ sub = L.d_strln "SUB: " ; L.d_increase_indent 1 ; Prop.d_sub sub ; @@ -1256,7 +1256,7 @@ end = struct (* optional print of missing: if print something, prepend with newline *) if !missing_pi <> [] || !missing_sigma <> [] || !missing_fld <> [] || !missing_typ <> [] || not (Sil.is_sub_empty sub) - then ( L.d_ln () ; L.d_str "[" ; _d_missing sub ; L.d_str "]" ) + then ( L.d_ln () ; L.d_str "[" ; d_missing_ sub ; L.d_str "]" ) let d_frame_fld () = @@ -1664,9 +1664,9 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2 and sexp_imply_nolhs tenv source calc_missing (subs: subst2) se2 typ2 = match se2 with - | Sil.Eexp (_e2, _) + | Sil.Eexp (e2_, _) -> ( - let e2 = Sil.exp_sub (`Exp (snd subs)) _e2 in + let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in match e2 with | Exp.Var v2 when Ident.is_primed v2 -> let v2' = path_to_id source in @@ -1679,7 +1679,7 @@ and sexp_imply_nolhs tenv source calc_missing (subs: subst2) se2 typ2 = else raise (IMPL_EXC ("exp only in rhs is not a primed var", subs, EXC_FALSE)) | Exp.Const _ when calc_missing -> let id = path_to_id source in - ProverState.add_missing_pi (Sil.Aeq (Exp.Var id, _e2)) ; + ProverState.add_missing_pi (Sil.Aeq (Exp.Var id, e2_)) ; subs | _ -> raise (IMPL_EXC ("exp only in rhs is not a primed var", subs, EXC_FALSE)) ) @@ -2109,9 +2109,9 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 : subst2 * Prop.normal Prop.t = match hpred2 with - | Sil.Hpointsto (_e2, se2, texp2) + | Sil.Hpointsto (e2_, se2, texp2) -> ( - let e2 = Sil.exp_sub (`Exp (snd subs)) _e2 in + let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in let _ = match e2 with | Exp.Lvar _ -> @@ -2146,7 +2146,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2) ; ( match fld_missing with | Some fld_missing -> - ProverState.add_missing_fld (Sil.Hpointsto (_e2, fld_missing, texp1)) + ProverState.add_missing_fld (Sil.Hpointsto (e2_, fld_missing, texp1)) | None -> () ) ; ( match fld_frame with @@ -2156,7 +2156,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 () ) ; ( match typing_missing with | Some t_missing -> - ProverState.add_missing_typ (_e2, t_missing) + ProverState.add_missing_typ (e2_, t_missing) | None -> () ) ; match typing_frame with @@ -2217,10 +2217,10 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 L.d_decrease_indent 1 ; res | _ -> assert false ) - | Sil.Hlseg (k, para2, _e2, _f2, _elist2) + | Sil.Hlseg (k, para2, e2_, f2_, elist2_) -> ( (* for now ignore implications between PE and NE *) - let e2, f2 = (Sil.exp_sub (`Exp (snd subs)) _e2, Sil.exp_sub (`Exp (snd subs)) _f2) in + let e2, f2 = (Sil.exp_sub (`Exp (snd subs)) e2_, Sil.exp_sub (`Exp (snd subs)) f2_) in let _ = match e2 with | Exp.Lvar _ -> @@ -2243,7 +2243,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 (filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2)) with | None -> - let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) _elist2 in + let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2_ in let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in L.d_increase_indent 1 ; let res = @@ -2253,13 +2253,13 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 (* calc_missing is false as we're checking an instantiation of the original list *) L.d_decrease_indent 1 ; res | Some iter1' -> - let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) _elist2 in + let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2_ in (* force instantiation of existentials *) let subs' = exp_list_imply tenv calc_missing subs (f2 :: elist2) (f2 :: elist2) in let prop1' = Prop.prop_iter_remove_curr_then_to_prop tenv iter1' in let hpred1 = match Prop.prop_iter_current tenv iter1' with hpred1, b -> - if b then ProverState.add_missing_pi (Sil.Aneq (_e2, _f2)) ; + if b then ProverState.add_missing_pi (Sil.Aneq (e2_, f2_)) ; (* for PE |- NE *) hpred1 in @@ -2269,9 +2269,9 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 | Sil.Hpointsto _ -> (* unroll rhs list and try again *) let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in - let _, para_inst2 = Sil.hpara_instantiate para2 _e2 n' elist2 in + let _, para_inst2 = Sil.hpara_instantiate para2 e2_ n' elist2 in let hpred_list2 = - para_inst2 @ [Prop.mk_lseg tenv Sil.Lseg_PE para2 n' _f2 _elist2] + para_inst2 @ [Prop.mk_lseg tenv Sil.Lseg_PE para2 n' f2_ elist2_] in L.d_increase_indent 1 ; let res = @@ -2279,7 +2279,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2 with exn when SymOp.exn_not_failure exn -> L.d_strln_color Red "backtracking lseg: trying rhs of length exactly 1" ; - let _, para_inst3 = Sil.hpara_instantiate para2 _e2 _f2 elist2 in + let _, para_inst3 = Sil.hpara_instantiate para2 e2_ f2_ elist2 in sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 ) in L.d_decrease_indent 1 ; res @@ -2355,9 +2355,9 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * Prop.normal Prop.t = let is_constant_string_class subs = function (* if the hpred represents a constant string, return the string *) - | Sil.Hpointsto (_e2, _, _) + | Sil.Hpointsto (e2_, _, _) -> ( - let e2 = Sil.exp_sub (`Exp (snd subs)) _e2 in + let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in match e2 with | Exp.Const Const.Cstr s -> Some (s, true) @@ -2488,10 +2488,10 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * L.d_decrease_indent 1 ; res in match hpred2 with - | Sil.Hpointsto (_e2, se2, t) -> + | Sil.Hpointsto (e2_, se2, t) -> let changed, calc_index_frame', hpred2' = expand_hpred_pointer tenv calc_index_frame - (Sil.Hpointsto (Prop.exp_normalize_noabs tenv (`Exp (snd subs)) _e2, se2, t)) + (Sil.Hpointsto (Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2_, se2, t)) in if changed then sigma_imply tenv calc_index_frame' calc_missing subs prop1 (hpred2' :: sigma2') @@ -2595,8 +2595,8 @@ let check_array_bounds tenv (sub1, sub2) prop = (* only check len *) in List.iter ~f:(fail_if_le len1) indices_to_check - | ProverState.BCfrom_pre _atom -> - let atom_neg = atom_negate tenv (Sil.atom_sub (`Exp sub2) _atom) in + | ProverState.BCfrom_pre atom_ -> + let atom_neg = atom_negate tenv (Sil.atom_sub (`Exp sub2) atom_) in (* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *) if check_atom tenv prop atom_neg then check_failed atom_neg in @@ -2737,15 +2737,15 @@ let is_cover tenv cases = incr cnt ; if Int.equal (!cnt mod 100) 0 then SymOp.check_wallclock_alarm () in - let rec _is_cover acc_pi cases = + let rec is_cover_ acc_pi cases = check () ; match cases with | [] -> check_inconsistency_pi tenv acc_pi | (pi, _) :: cases' -> - List.for_all ~f:(fun a -> _is_cover (atom_negate tenv a :: acc_pi) cases') pi + List.for_all ~f:(fun a -> is_cover_ (atom_negate tenv a :: acc_pi) cases') pi in - _is_cover [] cases + is_cover_ [] cases exception NO_COVER @@ -2763,15 +2763,15 @@ let find_minimum_pure_cover tenv cases = | (pi, x) :: todo' -> if is_cover tenv ((pi, x) :: seen) then (pi, x) :: seen else grow ((pi, x) :: seen) todo' in - let rec _shrink seen todo = + let rec shrink_ seen todo = match todo with | [] -> seen | (pi, x) :: todo' -> - if is_cover tenv (seen @ todo') then _shrink seen todo' - else _shrink ((pi, x) :: seen) todo' + if is_cover tenv (seen @ todo') then shrink_ seen todo' + else shrink_ ((pi, x) :: seen) todo' in - let shrink cases = if List.length cases > 2 then _shrink [] cases else cases in + let shrink cases = if List.length cases > 2 then shrink_ [] cases else cases in try Some (shrink (grow [] cases)) with NO_COVER -> None diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 7c53047ef..5c76b32a6 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -196,7 +196,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp for array accesses. This does not catch the array - bounds errors. If we want to implement the checks for array bounds errors, we need to change this function. *) -let rec _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se (typ: Typ.t) +let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se (typ: Typ.t) (off: Sil.offset list) inst = let new_id () = incr max_stamp ; @@ -207,10 +207,10 @@ let rec _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp [([], se, typ)] | [], Sil.Earray _, _ -> let off_new = Sil.Off_index Exp.zero :: off in - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst | (Off_fld _) :: _, Sil.Earray _, Tarray _ -> let off_new = Sil.Off_index Exp.zero :: off in - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst | (Off_fld (f, _)) :: off', Sil.Estruct (fsel, inst'), Tstruct name -> ( match Tenv.lookup tenv name with | Some ({fields; statics} as struct_typ) -> ( @@ -219,7 +219,7 @@ let rec _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp match List.find ~f:(fun (f', _) -> Typ.Fieldname.equal f f') fsel with | Some (_, se') -> let atoms_se_typ_list' = - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se' typ' + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in let replace acc (res_atoms', res_se', res_typ') = @@ -276,7 +276,7 @@ let rec _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp in let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in let typ_new = Typ.mk (Tarray (typ, None, None)) in - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst | (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ', stride) -> ( @@ -284,7 +284,7 @@ let rec _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with | Some (_, se') -> let atoms_se_typ_list' = - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se' typ' off' + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in let replace acc (res_atoms', res_se', res_typ') = @@ -356,7 +356,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp List.concat (List.rev (res_new :: acc)) | ((i, se) as ise) :: isel_unseen -> let atoms_se_typ_list = - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se typ_cont + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ_cont off inst in let atoms_se_typ_list' = @@ -425,7 +425,7 @@ let strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se t Sil.d_offset_list off' ; L.d_strln (if footprint_part then " FP" else " RE") ) ; let atoms_se_typ_list = - _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se typ off' inst + strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se typ off' inst in let atoms_se_typ_list_filtered = let check_neg_atom atom = diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 9eaecfcb0..f418ebf32 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -22,14 +22,14 @@ module F = Format (** Module for joined props *) module Jprop = struct (* type aliases for component of t values that compare should ignore *) - type _id = int + type id_ = int - let compare__id _ _ = 0 + let compare_id_ _ _ = 0 (** Remember when a prop is obtained as the join of two other props; the first parameter is an id *) type 'a t = - | Prop of _id * 'a Prop.t - | Joined of _id * 'a Prop.t * 'a t * 'a t + | Prop of id_ * 'a Prop.t + | Joined of id_ * 'a Prop.t * 'a t * 'a t [@@deriving compare] (** Comparison for joined_prop *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index cfec5f394..fad342755 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1082,10 +1082,10 @@ let execute_store ?(report_deref_errors= true) pname pdesc tenv lhs_exp typ rhs_ (** Execute [instr] with a symbolic heap [prop].*) -let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path +let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list = let current_pname = Procdesc.get_proc_name current_pdesc in - State.set_instr _instr ; + State.set_instr instr_ ; (* mark instruction last seen *) State.set_prop_tenv_pdesc prop_ tenv current_pdesc ; (* mark prop,tenv,pdesc last seen *) @@ -1096,7 +1096,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path List.map ~f:(fun p -> (p, path)) pl in let instr = - match _instr with + match instr_ with | Sil.Call (ret, exp, par, loc, call_flags) -> let exp' = Prop.exp_normalize_prop tenv prop_ exp in let instr' = @@ -1111,7 +1111,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path in instr' | _ -> - _instr + instr_ in let skip_call ?(is_objc_instance_method= false) ~reason prop path callee_pname ret_annots loc ret_id ret_typ_opt actual_args = diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index d7eb4e2dc..41cc22878 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -911,12 +911,12 @@ let combine tenv ret_id (posts: ('a Prop.t * Paths.Path.t) list) actual_pre path in post_p4 in - let _results = List.map ~f:(fun (p, path) -> (compute_result p, path)) instantiated_post in - if List.exists ~f:(fun (x, _) -> is_none x) _results then (* at least one combine failed *) + let results_ = List.map ~f:(fun (p, path) -> (compute_result p, path)) instantiated_post in + if List.exists ~f:(fun (x, _) -> is_none x) results_ then (* at least one combine failed *) None else let results = - List.map ~f:(function Some x, path -> (x, path) | None, _ -> assert false) _results + List.map ~f:(function Some x, path -> (x, path) | None, _ -> assert false) results_ in print_results tenv actual_pre (List.map ~f:fst results) ; Some results diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index d044aed40..bd5460b26 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -482,7 +482,7 @@ let wrappers_dir = lib_dir ^/ "wrappers" let ncpu = try - Utils.with_process_in "getconf _NPROCESSORS_ONLN 2>/dev/null" (fun chan -> + Utils.with_process_in "getconf NPROCESSORS_ONLN_ 2>/dev/null" (fun chan -> Scanf.bscanf (Scanf.Scanning.from_channel chan) "%d" (fun n -> n) ) |> fst with _ -> 1 diff --git a/infer/src/base/SourceFile.ml b/infer/src/base/SourceFile.ml index cbe0e8d77..aff24c6c9 100644 --- a/infer/src/base/SourceFile.ml +++ b/infer/src/base/SourceFile.ml @@ -30,9 +30,9 @@ let equal = [%compare.equal : t] module OrderedSourceFile = struct (* Don't use nonrec due to https://github.com/janestreet/ppx_compare/issues/2 *) - type _t = t [@@deriving compare] + type t_ = t [@@deriving compare] - type t = _t [@@deriving compare] + type t = t_ [@@deriving compare] end module Map = Caml.Map.Make (OrderedSourceFile) diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index a6a836e6b..19e94f5cb 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -11,13 +11,13 @@ open! IStd module F = Format module Raw = struct - type _typ = Typ.t + type typ_ = Typ.t - let compare__typ _ _ = 0 + let compare_typ_ _ _ = 0 (* ignore types while comparing bases. we can't trust the types from all of our frontends to be consistent, and the variable names should already be enough to distinguish the bases. *) - type base = Var.t * _typ [@@deriving compare] + type base = Var.t * typ_ [@@deriving compare] let equal_base = [%compare.equal : base] diff --git a/infer/src/checkers/idenv.ml b/infer/src/checkers/idenv.ml index 48c72d3a2..e33e3e673 100644 --- a/infer/src/checkers/idenv.ml +++ b/infer/src/checkers/idenv.ml @@ -36,8 +36,8 @@ let expand_expr idenv e = match e with Exp.Var id -> ( match lookup idenv id with Some e' -> e' | None -> e ) | _ -> e -let expand_expr_temps idenv node _exp = - let exp = expand_expr idenv _exp in +let expand_expr_temps idenv node exp_ = + let exp = expand_expr idenv exp_ in match exp with | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar -> ( match Errdesc.find_program_variable_assignment node pvar with diff --git a/infer/src/clang/ComponentKit.ml b/infer/src/clang/ComponentKit.ml index c5aa9199f..56fd3bf29 100644 --- a/infer/src/clang/ComponentKit.ml +++ b/infer/src/clang/ComponentKit.ml @@ -342,7 +342,7 @@ let is_in_factory_method (context: CLintersContext.context) = relies on other threads (dispatch_sync). Other side-effects, like reading of global variables, is not checked by this analyzer, although still an infraction of the rule. *) -let rec _component_initializer_with_side_effects_advice (context: CLintersContext.context) +let rec component_initializer_with_side_effects_advice_ (context: CLintersContext.context) call_stmt = let condition = in_ck_class context && is_in_factory_method context @@ -356,7 +356,7 @@ let rec _component_initializer_with_side_effects_advice (context: CLintersContex if condition then match call_stmt with | Clang_ast_t.ImplicitCastExpr (_, stmt :: _, _, _) -> - _component_initializer_with_side_effects_advice context stmt + component_initializer_with_side_effects_advice_ context stmt | Clang_ast_t.DeclRefExpr (_, _, _, decl_ref_expr_info) -> ( let refs = [decl_ref_expr_info.drti_decl_ref; decl_ref_expr_info.drti_found_decl_ref] in @@ -382,7 +382,7 @@ let rec _component_initializer_with_side_effects_advice (context: CLintersContex let component_initializer_with_side_effects_advice (context: CLintersContext.context) an = match an with | Ctl_parser_types.Stmt CallExpr (_, called_func_stmt :: _, _) -> - _component_initializer_with_side_effects_advice context called_func_stmt + component_initializer_with_side_effects_advice_ context called_func_stmt | _ -> None diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index b37b1bf75..9ad2cb38a 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -292,7 +292,7 @@ let rec apply_substitution f sub = ET (sub_list_param ntl, sw, apply_substitution f1 sub) -let expand_formula phi _map _error_msg = +let expand_formula phi map_ error_msg_ = let fail_with_circular_macro_definition name error_msg = L.(die ExternalError) "Macro '%s' has a circular definition.@\n Cycle:@\n%s" name error_msg in @@ -352,7 +352,7 @@ let expand_formula phi _map _error_msg = | ET (tl, sw, f1) -> ET (tl, sw, expand f1 map error_msg) in - expand phi _map _error_msg + expand phi map_ error_msg_ let rec expand_path paths path_map = @@ -368,7 +368,7 @@ let rec expand_path paths path_map = path :: expand_path rest path_map -let _build_macros_map macros init_map = +let build_macros_map_ macros init_map = let macros_map = List.fold ~f:(fun map' data -> @@ -387,7 +387,7 @@ let _build_macros_map macros init_map = let build_macros_map macros = let init_map : macros_map = ALVar.FormulaIdMap.empty in - _build_macros_map macros init_map + build_macros_map_ macros init_map let build_paths_map paths = @@ -411,7 +411,7 @@ let expand_checkers macro_map path_map checkers = let open CTL in let expand_one_checker c = L.(debug Linters Medium) " +Start expanding %s@\n" c.id ; - let map = _build_macros_map c.definitions macro_map in + let map = build_macros_map_ c.definitions macro_map in let exp_defs = List.fold ~f:(fun defs clause -> diff --git a/infer/src/clang/cPredicates.ml b/infer/src/clang/cPredicates.ml index b41eea8a8..e2e31c4ec 100644 --- a/infer/src/clang/cPredicates.ml +++ b/infer/src/clang/cPredicates.ml @@ -142,9 +142,9 @@ let captured_variables_cxx_ref an = type t = ALVar.formula_id * (* (name, [param1,...,paramK]) *) ALVar.alexp list [@@deriving compare] -let pp_predicate fmt (_name, _arglist) = - let name = ALVar.formula_id_to_string _name in - let arglist = List.map ~f:ALVar.alexp_to_string _arglist in +let pp_predicate fmt (name_, arglist_) = + let name = ALVar.formula_id_to_string name_ in + let arglist = List.map ~f:ALVar.alexp_to_string arglist_ in Format.fprintf fmt "%s(%a)" name (Pp.comma_seq Format.pp_print_string) arglist @@ -696,8 +696,8 @@ let get_ast_node_type_ptr an = CAst_utils.type_of_decl decl -let has_type an _typ = - match (get_ast_node_type_ptr an, _typ) with +let has_type an typ_ = + match (get_ast_node_type_ptr an, typ_) with | Some pt, ALVar.Const typ -> type_ptr_equal_type pt typ | _ -> @@ -721,9 +721,9 @@ let is_decl node = match node with Ctl_parser_types.Decl _ -> true | Ctl_parser_types.Stmt _ -> false -let method_return_type an _typ = +let method_return_type an typ_ = L.(debug Linters Verbose) "@\n Executing method_return_type..." ; - match (an, _typ) with + match (an, typ_) with | Ctl_parser_types.Decl Clang_ast_t.ObjCMethodDecl (_, _, mdi), ALVar.Const typ -> L.(debug Linters Verbose) "@\n with parameter `%s`...." typ ; let qual_type = mdi.Clang_ast_t.omdi_result_type in @@ -732,10 +732,10 @@ let method_return_type an _typ = false -let rec check_protocol_hiearachy decls_ptr _prot_name = +let rec check_protocol_hiearachy decls_ptr prot_name_ = let open Clang_ast_t in let is_this_protocol di_opt = - match di_opt with Some di -> ALVar.compare_str_with_alexp di.ni_name _prot_name | _ -> false + match di_opt with Some di -> ALVar.compare_str_with_alexp di.ni_name prot_name_ | _ -> false in match decls_ptr with | [] -> @@ -752,10 +752,10 @@ let rec check_protocol_hiearachy decls_ptr _prot_name = then true else let super_prot = List.map ~f:(fun dr -> dr.dr_decl_pointer) protocols in - check_protocol_hiearachy (super_prot @ decls') _prot_name + check_protocol_hiearachy (super_prot @ decls') prot_name_ -let has_type_subprotocol_of an _prot_name = +let has_type_subprotocol_of an prot_name_ = let open Clang_ast_t in let rec check_subprotocol t = match t with @@ -763,13 +763,13 @@ let has_type_subprotocol_of an _prot_name = check_subprotocol (CAst_utils.get_type qt.qt_type_ptr) | Some ObjCObjectType (_, ooti) -> if List.length ooti.ooti_protocol_decls_ptr > 0 then - check_protocol_hiearachy ooti.ooti_protocol_decls_ptr _prot_name + check_protocol_hiearachy ooti.ooti_protocol_decls_ptr prot_name_ else List.exists ~f:(fun qt -> check_subprotocol (CAst_utils.get_type qt.qt_type_ptr)) ooti.ooti_type_args | Some ObjCInterfaceType (_, pt) -> - check_protocol_hiearachy [pt] _prot_name + check_protocol_hiearachy [pt] prot_name_ | _ -> false in diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index bdf6e2366..d150e5a37 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -961,8 +961,8 @@ let choose_witness_opt witness_opt1 witness_opt2 = (* Evaluation of formulas *) (* evaluate an atomic formula (i.e. a predicate) on a ast node an and a linter context lcxt. That is: an, lcxt |= pred_name(params) *) -let rec eval_Atomic _pred_name args an lcxt = - let pred_name = ALVar.formula_id_to_string _pred_name in +let rec eval_Atomic pred_name_ args an lcxt = + let pred_name = ALVar.formula_id_to_string pred_name_ in match (pred_name, args, an) with | "call_class_method", [c; m], an -> CPredicates.call_class_method an c m diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 312d7c0a5..626d5f467 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -213,7 +213,7 @@ let collect_res_trans pdesc l = (* priority_node is used to enforce some kind of policy for creating nodes *) -(* in the cfg. Certain elements of the AST _must_ create nodes therefore *) +(* in the cfg. Certain elements of the AST must__ create nodes therefore *) (* there is no need for them to use priority_node. Certain elements *) (* instead need or need not to create a node depending of certain factors. *) (* When an element of the latter kind wants to create a node it must claim *) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index a6ae4d219..f700adfd2 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -1513,9 +1513,9 @@ module SyntacticQuotientedAccessListMap : QuotientedAccessListMap = struct module M = Caml.Map.Make (struct type t = RacerDDomain.Access.t - type _var = Var.t + type var_ = Var.t - let compare__var (u: Var.t) (v: Var.t) = + let compare_var_ (u: Var.t) (v: Var.t) = if phys_equal u v then 0 else match (u, v) with @@ -1532,7 +1532,7 @@ module SyntacticQuotientedAccessListMap : QuotientedAccessListMap = struct | (Read ap1 | Write ap1), (Read ap2 | Write ap2) | ( (ContainerRead (ap1, _) | ContainerWrite (ap1, _)) , (ContainerRead (ap2, _) | ContainerWrite (ap2, _)) ) -> - [%compare : (_var * Typ.t) * AccessPath.access list] ap1 ap2 + [%compare : (var_ * Typ.t) * AccessPath.access list] ap1 ap2 | (InterfaceCall _ | Read _ | Write _ | ContainerRead _ | ContainerWrite _), _ -> RacerDDomain.Access.compare x y diff --git a/infer/src/eradicate/models.ml b/infer/src/eradicate/models.ml index ae56ca4b7..3e6aadb5e 100644 --- a/infer/src/eradicate/models.ml +++ b/infer/src/eradicate/models.ml @@ -51,8 +51,8 @@ module Inference = struct string_of_int (n + 1) - let update_boolvec_str _s size index bval = - let s = if String.is_empty _s then String.make size '0' else _s in + let update_boolvec_str s_ size index bval = + let s = if String.is_empty s_ then String.make size '0' else s_ in s.[index] <- (if bval then '1' else '0') ; s diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index fc7d78371..e37a8fee2 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -258,8 +258,8 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get in (* Convert a complex expressions into a pvar. When [is_assigment] is true, update the relevant annotations for the pvar. *) - let convert_complex_exp_to_pvar node' is_assignment _exp typestate loc = - let exp = handle_field_access_via_temporary typestate (Idenv.expand_expr idenv _exp) in + let convert_complex_exp_to_pvar node' is_assignment exp_ typestate loc = + let exp = handle_field_access_via_temporary typestate (Idenv.expand_expr idenv exp_) in let default = (exp, typestate) in (* If this is an assignment, update the typestate for a field access pvar. *) let update_typestate_fld pvar origin fn typ = @@ -649,11 +649,11 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get in let handle_negated_condition cond_node = let do_instr = function[@warning "-57"] - | Sil.Prune (Exp.BinOp (Binop.Eq, _cond_e, Exp.Const Const.Cint i), _, _, _) - | Sil.Prune (Exp.BinOp (Binop.Eq, Exp.Const Const.Cint i, _cond_e), _, _, _) + | Sil.Prune (Exp.BinOp (Binop.Eq, cond_e_, Exp.Const Const.Cint i), _, _, _) + | Sil.Prune (Exp.BinOp (Binop.Eq, Exp.Const Const.Cint i, cond_e_), _, _, _) when IntLit.iszero i -> ( - let cond_e = Idenv.expand_expr_temps idenv cond_node _cond_e in + let cond_e = Idenv.expand_expr_temps idenv cond_node cond_e_ in match convert_complex_exp_to_pvar cond_node false cond_e typestate' loc with | Exp.Lvar pvar', _ -> set_flag pvar' AnnotatedSignature.Nullable false @@ -1058,30 +1058,30 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get None in (* Normalize the condition by resolving temp variables. *) - let rec normalize_cond _node _cond = - match _cond with + let rec normalize_cond node_ cond_ = + match cond_ with | Exp.UnOp (Unop.LNot, c, top) -> - let node', c' = normalize_cond _node c in + let node', c' = normalize_cond node_ c in (node', Exp.UnOp (Unop.LNot, c', top)) | Exp.BinOp (bop, c1, c2) -> - let node', c1' = normalize_cond _node c1 in + let node', c1' = normalize_cond node_ c1 in let node'', c2' = normalize_cond node' c2 in (node'', Exp.BinOp (bop, c1', c2')) | Exp.Var _ -> - let c' = Idenv.expand_expr idenv _cond in - if not (Exp.equal c' _cond) then normalize_cond _node c' else (_node, c') + let c' = Idenv.expand_expr idenv cond_ in + if not (Exp.equal c' cond_) then normalize_cond node_ c' else (node_, c') | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar -> ( match handle_assignment_in_condition pvar with | None -> ( - match Errdesc.find_program_variable_assignment _node pvar with + match Errdesc.find_program_variable_assignment node_ pvar with | Some (node', id) -> (node', Exp.Var id) | None -> - (_node, _cond) ) + (node_, cond_) ) | Some e2 -> - (_node, e2) ) + (node_, e2) ) | c -> - (_node, c) + (node_, c) in let node', ncond = normalize_cond node cond in check_condition node' ncond diff --git a/infer/src/scripts/checkCopyright.ml b/infer/src/scripts/checkCopyright.ml index dffc0de9e..be0b0e18d 100644 --- a/infer/src/scripts/checkCopyright.ml +++ b/infer/src/scripts/checkCopyright.ml @@ -157,9 +157,9 @@ let get_fb_year cstart cend lines_arr = !found -let pp_copyright mono fb_year com_style fmt _prefix = +let pp_copyright mono fb_year com_style fmt prefix_ = let running_comment = match com_style with Line (s, _) | Block (_, s, _) -> s in - let prefix = _prefix ^ running_comment in + let prefix = prefix_ ^ running_comment in let pp_line str = F.fprintf fmt "%s%s@\n" prefix str in let pp_start () = match com_style with @@ -173,7 +173,7 @@ let pp_copyright mono fb_year com_style fmt _prefix = | Line _ -> F.fprintf fmt "@\n" | Block (_, _, finish) -> - F.fprintf fmt "%s%s@\n" _prefix finish + F.fprintf fmt "%s%s@\n" prefix_ finish in pp_start () ; if mono then pp_line " Copyright (c) 2009 - 2013 Monoidics ltd." ;