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." ;