diff --git a/infer/src/IR/DecompiledExp.ml b/infer/src/IR/DecompiledExp.ml index b7a809d11..3bae4d8eb 100644 --- a/infer/src/IR/DecompiledExp.ml +++ b/infer/src/IR/DecompiledExp.ml @@ -68,7 +68,7 @@ let rec pp fmt = function F.fprintf fmt "*%a" pp de | Dfcall (fun_dexp, args, _, {cf_virtual= isvirtual}) -> let pp_args fmt des = - if eradicate_java () then (if des <> [] then F.pp_print_string fmt "...") + if eradicate_java () then (if not (List.is_empty des) then F.pp_print_string fmt "...") else Pp.comma_seq pp fmt des in let pp_fun fmt = function diff --git a/infer/src/IR/Fieldname.ml b/infer/src/IR/Fieldname.ml index cf1dcf069..f795cb63d 100644 --- a/infer/src/IR/Fieldname.ml +++ b/infer/src/IR/Fieldname.ml @@ -60,5 +60,5 @@ let is_java_outer_instance ({field_name} as field) = && let this = "this$" in let last_char = field_name.[String.length field_name - 1] in - (last_char >= '0' && last_char <= '9') + Char.(last_char >= '0' && last_char <= '9') && String.is_suffix field_name ~suffix:(this ^ String.of_char last_char) diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 45fac332b..77993d2e7 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -667,7 +667,7 @@ and eval_boolean_exp var = function | BinaryOperator (Binop.Eq, e1, e2) -> eval_boolean_binop Bool.equal var e1 e2 | BinaryOperator (Binop.Ne, e1, e2) -> - eval_boolean_binop ( <> ) var e1 e2 + eval_boolean_binop Bool.( <> ) var e1 e2 | _ -> (* non-boolean expression; can't evaluate it *) None diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml index 8335ea0f4..3bd686223 100644 --- a/infer/src/IR/IntLit.ml +++ b/infer/src/IR/IntLit.ml @@ -29,7 +29,7 @@ type t = {signedness: signedness; i: Z.t; pointerness: pointerness} [@@deriving exception OversizedShift let area {signedness; i} = - match (Z.(i < zero), signedness) with + match (Z.(lt i zero), signedness) with | true, Signed -> (* negative signed *) 1 | false, _ -> @@ -43,7 +43,7 @@ let to_signed intlit = | {signedness= Signed} -> Some intlit | {signedness= Unsigned; i} -> - if Z.(i < zero) then None else Some {intlit with signedness= Signed} + if Z.(lt i zero) then None else Some {intlit with signedness= Signed} let compare_value intlit1 intlit2 = diff --git a/infer/src/IR/Io_infer.ml b/infer/src/IR/Io_infer.ml index 32ff31a97..6d7f5903e 100644 --- a/infer/src/IR/Io_infer.ml +++ b/infer/src/IR/Io_infer.ml @@ -85,7 +85,7 @@ h1 { font-size:14pt } (** Return true if the html file was modified since the beginning of the analysis *) let modified_during_analysis source path = let fname = get_full_fname source path in - if DB.file_exists fname then DB.file_modified_time fname >= Config.initial_analysis_time + if DB.file_exists fname then Float.(DB.file_modified_time fname >= Config.initial_analysis_time) else false diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 9fa09cdcb..689b1adde 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -243,7 +243,7 @@ module Node = struct (** Append the instructions to the list of instructions to execute *) let append_instrs node instrs = - if instrs <> [] then node.instrs <- Instrs.append_list node.instrs instrs + if not (List.is_empty instrs) then node.instrs <- Instrs.append_list node.instrs instrs (** Map and replace the instructions to be executed *) @@ -466,7 +466,7 @@ let compute_distance_to_exit_node pdesc = next_nodes := node.preds @ !next_nodes in List.iter ~f:do_node nodes ; - if !next_nodes <> [] then mark_distance (dist + 1) !next_nodes + if not (List.is_empty !next_nodes) then mark_distance (dist + 1) !next_nodes in mark_distance 0 [exit_node] diff --git a/infer/src/IR/SpecializeProcdesc.ml b/infer/src/IR/SpecializeProcdesc.ml index 26a59dedf..f2752ba24 100644 --- a/infer/src/IR/SpecializeProcdesc.ml +++ b/infer/src/IR/SpecializeProcdesc.ml @@ -101,7 +101,7 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions = , (Exp.Var id, _) :: origin_args , loc , call_flags ) - when call_flags.CallFlags.cf_virtual && redirect_typename id <> None -> + when call_flags.CallFlags.cf_virtual && Option.is_some (redirect_typename id) -> let redirected_typename = Option.value_exn (redirect_typename id) in let redirected_typ = mk_ptr_typ redirected_typename in let redirected_pname = Procname.replace_class callee_pname redirected_typename in diff --git a/infer/src/IR/Subtype.ml b/infer/src/IR/Subtype.ml index 0a39bd724..502e9602c 100644 --- a/infer/src/IR/Subtype.ml +++ b/infer/src/IR/Subtype.ml @@ -17,7 +17,7 @@ let list_to_string list = type t' = Exact (** denotes the current type only *) | Subtypes of Typ.Name.t list -[@@deriving compare] +[@@deriving compare, equal] let equal_modulo_flag (st1, _) (st2, _) = [%compare.equal: t'] st1 st2 @@ -26,7 +26,7 @@ type kind = CAST | INSTOF | NORMAL [@@deriving compare] let equal_kind = [%compare.equal: kind] -type t = t' * kind [@@deriving compare] +type t = t' * kind [@@deriving compare, equal] type result = No | Unknown | Yes [@@deriving compare] diff --git a/infer/src/IR/Subtype.mli b/infer/src/IR/Subtype.mli index fc312813d..186498c66 100644 --- a/infer/src/IR/Subtype.mli +++ b/infer/src/IR/Subtype.mli @@ -11,7 +11,7 @@ open! IStd module F = Format -type t [@@deriving compare] +type t [@@deriving compare, equal] val pp : F.formatter -> t -> unit diff --git a/infer/src/al/CiOSVersionNumbers.ml b/infer/src/al/CiOSVersionNumbers.ml index 649e0c859..fa35ce924 100644 --- a/infer/src/al/CiOSVersionNumbers.ml +++ b/infer/src/al/CiOSVersionNumbers.ml @@ -54,6 +54,7 @@ let sort_versions versions = let version_of number_s : human_readable_version option = let epsilon = 0.001 in let rec version_of_aux version_numbers number = + let open Float in match version_numbers with | (version_n, version_s) :: (next_version_n, next_version_s) :: rest -> if number -. version_n < epsilon && number -. version_n > ~-.epsilon then Some version_s diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index a543b63fc..42f6b99d0 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -361,7 +361,7 @@ let pp_custom_of_report fmt report fields = let pp_trace fmt trace comma = let pp_trace_elem fmt {description} = F.pp_print_string fmt description in let trace_without_empty_descs = - List.filter ~f:(fun {description} -> description <> "") trace + List.filter ~f:(fun {description} -> not (String.is_empty description)) trace in F.fprintf fmt "%s[%a]" comma (Pp.comma_seq pp_trace_elem) trace_without_empty_descs in @@ -504,7 +504,7 @@ module Stats = struct let code = match Printer.LineReader.from_loc linereader loc with Some s -> s | None -> "" in let line = let pp fmt = - if description <> "" then + if not (String.is_empty description) then F.fprintf fmt "%s%4s // %s@\n" (indent_string (level + indent_num)) " " description ; F.fprintf fmt "%s%04d: %s" (indent_string (level + indent_num)) loc.Location.line code in @@ -553,7 +553,7 @@ module Stats = struct process_err_log error_filter linereader (Summary.get_err_log summary) stats in let is_defective = found_errors in - let is_verified = specs <> [] && not is_defective in + let is_verified = (not (List.is_empty specs)) && not is_defective in let is_checked = not (is_defective || is_verified) in let is_timeout = match Summary.(Stats.failure_kind summary.stats) with diff --git a/infer/src/backend/SpecsFiles.ml b/infer/src/backend/SpecsFiles.ml index 2647794aa..65c632520 100644 --- a/infer/src/backend/SpecsFiles.ml +++ b/infer/src/backend/SpecsFiles.ml @@ -13,7 +13,8 @@ module CLOpt = CommandLineOption let load_specfiles () = let specs_files_in_dir dir = let is_specs_file fname = - Sys.is_directory fname <> `Yes && Filename.check_suffix fname Config.specs_files_suffix + PolyVariantEqual.(Sys.is_directory fname <> `Yes) + && Filename.check_suffix fname Config.specs_files_suffix in match Sys.readdir dir with | exception Sys_error _ -> @@ -38,8 +39,8 @@ let spec_files_from_cmdline () = files may be generated between init and report time. *) List.iter ~f:(fun arg -> - if (not (Filename.check_suffix arg Config.specs_files_suffix)) && arg <> "." then - print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") ) + if (not (Filename.check_suffix arg Config.specs_files_suffix)) && not (String.equal arg ".") + then print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") ) Config.anon_args ; if Config.test_filtering then (Inferconfig.test () ; L.exit 0) ; if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args ) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 543b2994c..360f18c85 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -71,7 +71,7 @@ let iterate_procedure_callbacks exe_env summary = (** Invoke all registered cluster callbacks on a cluster of procedures. *) let iterate_cluster_callbacks procedures exe_env source_file = - if !cluster_callbacks <> [] then + if not (List.is_empty !cluster_callbacks) then let environment = {procedures; source_file; exe_env} in let language_matches language = match procedures with diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 405bbca72..911d1d1b9 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -140,7 +140,7 @@ let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = let find_instr n = let filter = function | Sil.Store {e1= Exp.Lvar pvar_; e2= Exp.Const (Const.Cint i)} when Pvar.equal pvar pvar_ -> - IntLit.iszero i <> true_branch + Bool.(IntLit.iszero i <> true_branch) | _ -> false in @@ -462,7 +462,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = let node_instrs = Procdesc.Node.get_instrs node in let hpred_typ_opt = find_hpred_typ hpred in let value_str_from_pvars_vpath pvars vpath = - if pvars <> [] then + if not (List.is_empty pvars) then let pp = Pp.seq Pvar.pp_value in let desc_string = F.asprintf "%a" pp pvars in Some desc_string @@ -554,7 +554,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (* we know it has been allocated *) (Exceptions.Exn_user, bucket) | None -> - if leak_from_list_abstraction hpred prop && value_str <> None then + if leak_from_list_abstraction hpred prop && Option.is_some value_str then (* we don't know it's been allocated, but it's coming from list abstraction and we have a name *) (Exceptions.Exn_user, bucket) diff --git a/infer/src/base/CommandLineOption.ml b/infer/src/base/CommandLineOption.ml index 849545242..bc13c5ea8 100644 --- a/infer/src/base/CommandLineOption.ml +++ b/infer/src/base/CommandLineOption.ml @@ -11,12 +11,13 @@ open! IStd module F = Format module YBU = Yojson.Basic.Util module L = Die +open PolyVariantEqual let ( = ) = String.equal let manpage_s_notes = "NOTES" -let is_env_var_set v = Option.value (Option.map (Sys.getenv v) ~f:(( = ) "1")) ~default:false +let is_env_var_set v = Option.value (Option.map (Sys.getenv v) ~f:(String.equal "1")) ~default:false (** The working directory of the initial invocation of infer, to which paths passed as command line options are relative. *) @@ -147,7 +148,7 @@ let check_no_duplicates desc_list = let rec check_for_duplicates_ = function | [] | [_] -> true - | (x, _, _) :: (y, _, _) :: _ when x <> "" && x = y -> + | (x, _, _) :: (y, _, _) :: _ when (not (String.is_empty x)) && x = y -> L.(die InternalError) "Multiple definitions of command line option: %s" x | _ :: tl -> check_for_duplicates_ tl @@ -243,7 +244,7 @@ let deprecate_desc parse_mode ~long ~short ~deprecated doc desc = match parse_mode with | Javac | NoParse -> () - | InferCommand when long <> "" -> + | InferCommand when not (String.is_empty long) -> warnf "WARNING:%s '-%s' is deprecated. Use '--%s'%s instead.@." source_s deprecated long (if short = "" then "" else Printf.sprintf " or '-%s'" short) | InferCommand -> @@ -290,9 +291,9 @@ let mk ?(deprecated = []) ?(parse_mode = InferCommand) ?(in_help = []) ~long ?sh let short = match short0 with Some c -> String.of_char c | None -> "" in let desc = {long; short; meta; doc; default_string; spec; decode_json} in (* add desc for long option, with documentation (which includes any short option) for exes *) - if long <> "" then add parse_mode in_help desc ; + if not (String.is_empty long) then add parse_mode in_help desc ; (* add desc for short option only for parsing, without documentation *) - if short <> "" then add parse_mode [] {desc with long= ""; meta= ""; doc= ""} ; + if not (String.is_empty short) then add parse_mode [] {desc with long= ""; meta= ""; doc= ""} ; (* add desc for deprecated options only for parsing, without documentation *) List.iter deprecated ~f:(fun deprecated -> deprecate_desc parse_mode ~long ~short ~deprecated doc desc |> add parse_mode [] ) ; @@ -1010,7 +1011,7 @@ let parse ?config_file ~usage action initial_command = in let to_export = let argv_to_export = decode_env_to_argv !args_to_export in - if argv_to_export <> [] then ( + if not (List.is_empty argv_to_export) then ( (* We have to be careful not to add too much data to the environment because the size of the environment contributes to the length of the command to be run. If the environment + CLI is too big, running any command will fail with a cryptic "exit code 127" error. Use an argfile @@ -1040,7 +1041,7 @@ let wrap_line indent_string wrap_length line0 = else len in let new_length = line_length + String.length word_sep_str + word_length in - let new_non_empty = non_empty || word <> "" in + let new_non_empty = non_empty || not (String.is_empty word) in if new_length > wrap_length && non_empty then (line :: rev_lines, true, indent_string ^ word, indent_length + word_length) else diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index f44e541b5..eb3297bba 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2585,7 +2585,7 @@ let post_parsing_initialization command_opt = CommandDoc.infer command_opt | `None -> () ) ; - if !version <> `None || !help <> `None then Stdlib.exit 0 ; + if PolyVariantEqual.(!version <> `None || !help <> `None) then Stdlib.exit 0 ; let uncaught_exception_handler exn raw_backtrace = let is_infer_exit_zero = match exn with L.InferExit 0 -> true | _ -> false in let should_print_backtrace_default = diff --git a/infer/src/base/RunState.ml b/infer/src/base/RunState.ml index b7ac25ac1..57b7ea735 100644 --- a/infer/src/base/RunState.ml +++ b/infer/src/base/RunState.ml @@ -50,7 +50,7 @@ let load_and_validate () = Was it created using an older version of infer?" Config.results_dir err_msg) ) msg in - if Sys.file_exists state_file_path <> `Yes then + if PolyVariantEqual.(Sys.file_exists state_file_path <> `Yes) then error "save state not found: '%s' does not exist" state_file_path else match Atdgen_runtime.Util.Json.from_file Runstate_j.read_t state_file_path with diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index ef1450366..dec58ce4a 100644 --- a/infer/src/base/SymOp.ml +++ b/infer/src/base/SymOp.ml @@ -113,7 +113,7 @@ let unset_wallclock_alarm () = !gs.last_wallclock <- None (** if the wallclock alarm has expired, raise a timeout exception *) let check_wallclock_alarm () = match (!gs.last_wallclock, !wallclock_timeout_handler) with - | Some alarm_time, Some handler when Unix.gettimeofday () >= alarm_time -> + | Some alarm_time, Some handler when Float.(Unix.gettimeofday () >= alarm_time) -> unset_wallclock_alarm () ; handler () | _ -> () @@ -123,7 +123,7 @@ let check_wallclock_alarm () = let get_remaining_wallclock_time () = match !gs.last_wallclock with | Some alarm_time -> - max 0.0 (alarm_time -. Unix.gettimeofday ()) + Float.(max 0.0 (alarm_time -. Unix.gettimeofday ())) | None -> 0.0 diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index 25d4ec344..abed01c20 100644 --- a/infer/src/base/Utils.ml +++ b/infer/src/base/Utils.ml @@ -265,10 +265,12 @@ let with_process_lines ~(debug : ('a, F.formatter, unit) format -> 'a) ~cmd ~tmp shell_cmd output +let is_dir_kind (kind : Unix.file_kind) = match kind with S_DIR -> true | _ -> false + (** Recursively create a directory if it does not exist already. *) let create_dir dir = try - if (Unix.stat dir).Unix.st_kind <> Unix.S_DIR then + if not (is_dir_kind (Unix.stat dir).Unix.st_kind) then L.(die ExternalError) "file '%s' already exists and is not a directory" dir with Unix.Unix_error _ -> ( try Unix.mkdir_p dir ~perm:0o700 diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index b7505bedf..415c6d208 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -1124,7 +1124,7 @@ let check_junk pname tenv prop = | Some _, None | None, Some _ -> false in - (is_none alloc_attribute && !leaks_reported <> []) + (is_none alloc_attribute && not (List.is_empty !leaks_reported)) || (* None attribute only reported if it's the first one *) List.mem ~equal:attr_opt_equal !leaks_reported alloc_attribute in diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml index 39fe82c74..1c5e5702a 100644 --- a/infer/src/biabduction/Dom.ml +++ b/infer/src/biabduction/Dom.ml @@ -1487,7 +1487,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop 'todo' describes the start point. *) let cut_sigma side todo (target : Prop.sigma) (other : Prop.sigma) = let list_is_empty l = - if l <> [] then (L.d_strln "failure reason 61" ; raise Predicates.JoinFail) + if not (List.is_empty l) then (L.d_strln "failure reason 61" ; raise Predicates.JoinFail) in let x = Todo.take () in Todo.push todo ; diff --git a/infer/src/biabduction/Match.ml b/infer/src/biabduction/Match.ml index e5f351b53..14c5fc790 100644 --- a/infer/src/biabduction/Match.ml +++ b/infer/src/biabduction/Match.ml @@ -722,7 +722,7 @@ let rec generic_find_partial_iso tenv mode update corres sigma_corres todos sigm new_sigma_todo ) | ( Some (Predicates.Hlseg (k1, para1, root1, next1, shared1) as hpred1) , Some (Predicates.Hlseg (k2, para2, root2, next2, shared2) as hpred2) ) -> ( - if k1 <> k2 || not (hpara_iso tenv para1 para2) then None + if (not (Predicates.equal_lseg_kind k1 k2)) || not (hpara_iso tenv para1 para2) then None else try let new_corres = @@ -747,7 +747,8 @@ let rec generic_find_partial_iso tenv mode update corres sigma_corres todos sigm with Invalid_argument _ -> None ) | ( Some (Predicates.Hdllseg (k1, para1, iF1, oB1, oF1, iB1, shared1) as hpred1) , Some (Predicates.Hdllseg (k2, para2, iF2, oB2, oF2, iB2, shared2) as hpred2) ) -> ( - if k1 <> k2 || not (hpara_dll_iso tenv para1 para2) then None + if (not (Predicates.equal_lseg_kind k1 k2)) || not (hpara_dll_iso tenv para1 para2) then + None else try let new_corres = diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index 953cb8fa3..43c6ab56f 100644 --- a/infer/src/biabduction/Paths.ml +++ b/infer/src/biabduction/Paths.ml @@ -281,7 +281,7 @@ end = struct f level path session prev_exn_opt | Pnode (_, exn_opt, session', p, _, _) -> (* no two consecutive exceptions *) - let next_exn_opt = if prev_exn_opt <> None then None else exn_opt in + let next_exn_opt = if Option.is_some prev_exn_opt then None else exn_opt in doit level (session' :> int) p next_exn_opt ; f level path session prev_exn_opt | Pjoin (p1, p2, _) -> @@ -316,7 +316,8 @@ end = struct PredSymb.equal_path_pos (get_path_pos node) pos in let path_pos_at_path p = - try match curr_node p with Some node -> pos_opt <> None && filter node | None -> false + try + match curr_node p with Some node -> Option.is_some pos_opt && filter node | None -> false with exn when SymOp.exn_not_failure exn -> false in let position_seen = ref false in @@ -527,7 +528,7 @@ end = struct (lt1.Errlog.lt_level, lt1.Errlog.lt_loc) (lt2.Errlog.lt_level, lt2.Errlog.lt_loc) in - let relevant lt = lt.Errlog.lt_node_tags <> [] in + let relevant lt = not (List.is_empty lt.Errlog.lt_node_tags) in IList.remove_irrelevant_duplicates ~equal ~f:relevant (List.rev !trace) end diff --git a/infer/src/biabduction/Predicates.ml b/infer/src/biabduction/Predicates.ml index f8535a107..0e572cbbd 100644 --- a/infer/src/biabduction/Predicates.ml +++ b/infer/src/biabduction/Predicates.ml @@ -308,7 +308,7 @@ end = struct already. This can in turn extend the todo list for the nested predicates, which are then visited as well. Can be applied only once, as it destroys the todo list *) let iter (env : t) f f_dll = - while env.todo <> [] || env.todo_dll <> [] do + while (not (List.is_empty env.todo)) || not (List.is_empty env.todo_dll) do match env.todo with | hpara :: todo' -> env.todo <- todo' ; diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index 5cef857d5..3254ab1c6 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -188,15 +188,15 @@ 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 ~compare:Predicates.compare_hpred sg_ in - if sg <> [] then (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) fmt sg + if not (List.is_empty sg) then (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) fmt sg in let pp_nl fmt doit = if doit then Format.fprintf fmt " ;@\n" in let pp_nonstack fmt = Pp.semicolon_seq ~print_env:pe (Predicates.pp_hpred_env pe (Some env)) fmt in - if sigma_stack <> [] || sigma_nonstack <> [] then + if (not (List.is_empty sigma_stack)) || not (List.is_empty sigma_nonstack) then Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl - (sigma_stack <> [] && sigma_nonstack <> []) + ((not (List.is_empty sigma_stack)) && not (List.is_empty sigma_nonstack)) pp_nonstack sigma_nonstack @@ -205,7 +205,9 @@ let d_sigma (sigma : sigma) = L.d_pp_with_pe pp_sigma sigma (** Dump a pi and a sigma *) let d_pi_sigma pi sigma = - let d_separator () = if pi <> [] && sigma <> [] then L.d_strln " *" in + let d_separator () = + if (not (List.is_empty pi)) && not (List.is_empty sigma) then L.d_strln " *" + in d_pi pi ; d_separator () ; d_sigma sigma @@ -244,7 +246,9 @@ let get_pure_extended p = (** Print existential quantification *) -let pp_evars f evars = if evars <> [] then F.fprintf f "exists [%a]. " (Pp.comma_seq Ident.pp) evars +let pp_evars f evars = + if not (List.is_empty evars) then F.fprintf f "exists [%a]. " (Pp.comma_seq Ident.pp) evars + (** Print an hpara in simple mode *) let pp_hpara_simple pe_ env n f pred = @@ -287,8 +291,8 @@ let prop_update_obj_sub pe prop = Pp.set_obj_sub pe (create_pvar_env prop.sigma) (** 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_pure f pi = if pi <> [] then F.fprintf f "%a *@\n" (pp_pi pe) pi in - if fp.pi_fp <> [] || fp.sigma_fp <> [] then + let pp_pure f pi = if not (List.is_empty pi) then F.fprintf f "%a *@\n" (pp_pi pe) pi in + if (not (List.is_empty fp.pi_fp)) || not (List.is_empty fp.sigma_fp) then F.fprintf f "@\n[footprint@\n @[%a%a@] ]" pp_pure fp.pi_fp (pp_sigma_simple pe env) fp.sigma_fp @@ -309,8 +313,8 @@ let pp_prop pe0 f prop = (* since prop diff is based on physical equality, we need to extract the sub verbatim *) let pi = prop.pi in let pp_pure f () = - if subl <> [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl ; - if pi <> [] then F.fprintf f "%a ;@\n" (pp_pi pe) pi + if not (List.is_empty subl) then F.fprintf f "%a ;@\n" (pp_subl pe) subl ; + if not (List.is_empty pi) then F.fprintf f "%a ;@\n" (pp_pi pe) pi in let env = prop_pred_env prop in let iter_f n hpara = F.fprintf f "@,@[%a@]" (pp_hpara_simple pe env n) hpara in @@ -720,7 +724,7 @@ module Normalize = struct | Const (Cint n), Const (Cint m) -> Exp.bool (IntLit.leq n m) | Const (Cfloat v), Const (Cfloat w) -> - Exp.bool (v <= w) + Exp.bool Float.(v <= w) | BinOp (PlusA _, e3, Const (Cint n)), Const (Cint m) -> BinOp (Le, e3, Exp.int (m -- n)) | e1', e2' -> @@ -730,7 +734,7 @@ module Normalize = struct | Const (Cint n), Const (Cint m) -> Exp.bool (IntLit.lt n m) | Const (Cfloat v), Const (Cfloat w) -> - Exp.bool (v < w) + Exp.bool Float.(v < w) | Const (Cint n), BinOp ((MinusA _ as ominus), f1, f2) -> BinOp (Le, BinOp (ominus, f2, f1), Exp.int (IntLit.minus_one -- n)) | BinOp ((MinusA _ as ominus), f1, f2), Const (Cint n) -> @@ -760,7 +764,7 @@ module Normalize = struct | Const (Cint n), Const (Cint m) -> Exp.bool (IntLit.neq n m) | Const (Cfloat v), Const (Cfloat w) -> - Exp.bool (v <> w) + Exp.bool Float.(v <> w) | Const (Cint _), Exp.Lvar _ | Exp.Lvar _, Const (Cint _) -> (* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *) (* Assume they are not equal *) diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 82dafa580..9c31b598b 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -737,7 +737,7 @@ let check_disequal tenv prop e1 e2 = let sigma_rest' = List.rev_append sigma_irrelevant sigma_rest in f [] e2 sigma_rest' ) | Predicates.Hdllseg (Lseg_NE, _, iF, _, _, iB, _) :: sigma_rest -> - if is_root tenv prop iF e <> None || is_root tenv prop iB e <> None then + if Option.is_some (is_root tenv prop iF e) || Option.is_some (is_root tenv prop iB e) then let sigma_irrelevant' = List.rev_append sigma_irrelevant sigma_rest in Some (true, sigma_irrelevant') else @@ -870,16 +870,16 @@ let check_allocatedness tenv prop e = let spatial_part = prop.Prop.sigma in let f = function | Predicates.Hpointsto (base, _, _) -> - is_root tenv prop base n_e <> None + Option.is_some (is_root tenv prop base n_e) | Predicates.Hlseg (k, _, e1, e2, _) -> if Predicates.equal_lseg_kind k Lseg_NE || check_disequal tenv prop e1 e2 then - is_root tenv prop e1 n_e <> None + Option.is_some (is_root tenv prop e1 n_e) else false | Predicates.Hdllseg (k, _, iF, oB, oF, iB, _) -> if Predicates.equal_lseg_kind k Lseg_NE || check_disequal tenv prop iF oF || check_disequal tenv prop iB oB - then is_root tenv prop iF n_e <> None || is_root tenv prop iB n_e <> None + then Option.is_some (is_root tenv prop iF n_e) || Option.is_some (is_root tenv prop iB n_e) else false in List.exists ~f spatial_part @@ -1186,17 +1186,17 @@ end = struct L.d_increase_indent () ; Prop.d_sub sub ; L.d_decrease_indent () ; - if !missing_pi <> [] && !missing_sigma <> [] then ( + if (not (List.is_empty !missing_pi)) && not (List.is_empty !missing_sigma) then ( L.d_ln () ; Prop.d_pi !missing_pi ; L.d_strln "*" ; Prop.d_sigma !missing_sigma ) - else if !missing_pi <> [] then (L.d_ln () ; Prop.d_pi !missing_pi) - else if !missing_sigma <> [] then (L.d_ln () ; Prop.d_sigma !missing_sigma) ; - if !missing_fld <> [] then ( + else if not (List.is_empty !missing_pi) then (L.d_ln () ; Prop.d_pi !missing_pi) + else if not (List.is_empty !missing_sigma) then (L.d_ln () ; Prop.d_sigma !missing_sigma) ; + if not (List.is_empty !missing_fld) then ( L.d_ln () ; L.d_strln "MISSING FLD:" ; L.d_increase_indent () ; Prop.d_sigma !missing_fld ; L.d_decrease_indent () ) ; - if !missing_typ <> [] then ( + if not (List.is_empty !missing_typ) then ( L.d_ln () ; L.d_strln "MISSING TYPING:" ; L.d_increase_indent () ; @@ -1207,14 +1207,17 @@ end = struct let d_missing sub = (* optional print of missing: if print something, prepend with newline *) if - !missing_pi <> [] || !missing_sigma <> [] || !missing_fld <> [] || !missing_typ <> [] + (not (List.is_empty !missing_pi)) + || (not (List.is_empty !missing_sigma)) + || (not (List.is_empty !missing_fld)) + || (not (List.is_empty !missing_typ)) || not (Predicates.is_sub_empty sub) then ( L.d_ln () ; L.d_str "[" ; d_missing_ sub ; L.d_str "]" ) let d_frame_fld () = (* optional print of frame fld: if print something, prepend with newline *) - if !frame_fld <> [] then ( + if not (List.is_empty !frame_fld) then ( L.d_ln () ; L.d_strln "[FRAME FLD:" ; L.d_increase_indent () ; @@ -1225,7 +1228,7 @@ end = struct let d_frame_typ () = (* optional print of frame typ: if print something, prepend with newline *) - if !frame_typ <> [] then ( + if not (List.is_empty !frame_typ) then ( L.d_ln () ; L.d_strln "[FRAME TYPING:" ; L.d_increase_indent () ; @@ -1469,10 +1472,11 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 : struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 in let fld_frame_opt = - if fld_frame <> [] then Some (Predicates.Estruct (fld_frame, inst1)) else None + if not (List.is_empty fld_frame) then Some (Predicates.Estruct (fld_frame, inst1)) else None in let fld_missing_opt = - if fld_missing <> [] then Some (Predicates.Estruct (fld_missing, inst1)) else None + if not (List.is_empty fld_missing) then Some (Predicates.Estruct (fld_missing, inst1)) + else None in (subs', fld_frame_opt, fld_missing_opt) | Predicates.Estruct _, Predicates.Eexp (e2, _) -> ( @@ -1492,10 +1496,11 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 : array_imply tenv source calc_index_frame calc_missing subs' esel1 esel2 typ2 in let index_frame_opt = - if index_frame <> [] then Some (Predicates.Earray (len1, index_frame, inst1)) else None + if not (List.is_empty index_frame) then Some (Predicates.Earray (len1, index_frame, inst1)) + else None in let index_missing_opt = - if index_missing <> [] && !BiabductionConfig.footprint then + if (not (List.is_empty index_missing)) && !BiabductionConfig.footprint then Some (Predicates.Earray (len1, index_missing, inst1)) else None in @@ -1839,7 +1844,7 @@ module Subtyping_check = struct when ( Typ.Name.equal cn1 Typ.Name.Java.java_io_serializable || Typ.Name.equal cn1 Typ.Name.Java.java_lang_cloneable || Typ.Name.equal cn1 Typ.Name.Java.java_lang_object ) - && st1 <> Subtype.exact -> + && not (Subtype.equal st1 Subtype.exact) -> (Some st1, None) | Tstruct cn1, Tstruct cn2 (* cn1 <: cn2 or cn2 <: cn1 is implied in Java when we get two types compared *) @@ -2528,7 +2533,8 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 Prop.d_pi pi2 ; L.d_decrease_indent () ; L.d_ln () ; - if pi2_bcheck <> [] then (L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; L.d_ln ()) ; + if not (List.is_empty pi2_bcheck) then ( + L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; L.d_ln () ) ; L.d_strln "returns" ; L.d_strln "sub1:" ; L.d_increase_indent () ; @@ -2556,7 +2562,8 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 L.d_ln () ; L.d_strln "returning TRUE" ; let frame = frame_prop.Prop.sigma in - if check_frame_empty && frame <> [] then raise (IMPL_EXC ("frame not empty", subs, EXC_FALSE)) ; + if check_frame_empty && not (List.is_empty frame) then + raise (IMPL_EXC ("frame not empty", subs, EXC_FALSE)) ; Some ((sub1, sub2), frame) with | IMPL_EXC (s, subs, body) -> diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index f714d9d46..83c2404f5 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -951,7 +951,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc = false ) prop.Prop.sigma in - Procdesc.get_access pdesc <> PredSymb.Private + (not (PredSymb.equal_access (Procdesc.get_access pdesc) Private)) && (not (Annotations.pdesc_return_annot_ends_with pdesc Annotations.visibleForTesting)) && (not ( match Procdesc.get_proc_name pdesc with @@ -1513,9 +1513,7 @@ let is_only_pt_by_fld_or_param_with_annot pdesc tenv prop deref_exp is_annotatio | _ -> true in - if List.for_all ~f:is_pt_by_fld_or_param_with_annot prop.Prop.sigma && !obj_str <> None then - !obj_str - else None + if List.for_all ~f:is_pt_by_fld_or_param_with_annot prop.Prop.sigma then !obj_str else None let is_only_pt_by_fld_or_param_nullable pdesc tenv prop deref_exp = diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 191e56807..8a9f455b2 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -594,7 +594,7 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t (* if this is not a virtual or interface call, there's no need for resolution *) [callee_pname] | (receiver_exp, actual_receiver_typ) :: _ -> - if !Language.curr_language <> Language.Java then + if not (Language.curr_language_is Java) then (* default mode for Obj-C/C++/Java virtual calls: resolution only *) [do_resolve callee_pname receiver_exp actual_receiver_typ] else @@ -1264,7 +1264,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t | Sil.Prune (cond, loc, true_branch, ik) -> let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in let check_condition_always_true_false () = - if !Language.curr_language <> Language.Clang || Config.report_condition_always_true_in_clang + if (not (Language.curr_language_is Clang)) || Config.report_condition_always_true_in_clang then let report_condition_always_true_false i = let skip_loop = @@ -2010,9 +2010,12 @@ let node handle_exn exe_env tenv summary proc_cfg (node : ProcCfg.Exceptional.No if Tabulation.prop_is_exn pname p && (not (Sil.instr_is_auxiliary instr)) - && ProcCfg.Exceptional.Node.kind node <> Procdesc.Node.exn_handler_kind - (* skip normal instructions if an exception was thrown, - unless this is an exception handler node *) + && not + (Procdesc.Node.equal_nodekind + (ProcCfg.Exceptional.Node.kind node) + Procdesc.Node.exn_handler_kind) + (* skip normal instructions if an exception was thrown, unless this is an exception + handler node *) then ( L.d_str "Skipping instr " ; Sil.d_instr instr ; diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index f82c74edc..3a6f4b25f 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -385,7 +385,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo None else None in - if deref_no_null_check_pos <> None then + if Option.is_some deref_no_null_check_pos then (* only report a dereference null error if we know there was a dereference without null check *) match deref_no_null_check_pos with @@ -871,12 +871,12 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat L.d_strln "Frame fld:" ; Prop.d_sigma split.frame_fld ; L.d_ln () ; - if split.frame_typ <> [] then ( + if not (List.is_empty split.frame_typ) then ( L.d_strln "Frame typ:" ; Prover.d_typings split.frame_typ ; L.d_ln () ) ; L.d_strln "Missing fld:" ; Prop.d_sigma split.missing_fld ; L.d_ln () ; - if split.missing_typ <> [] then ( + if not (List.is_empty split.missing_typ) then ( L.d_strln "Missing typ:" ; Prover.d_typings split.missing_typ ; L.d_ln () ) ; @@ -984,7 +984,7 @@ let mk_actual_precondition tenv prop actual_params formal_params = | f :: fpars', a :: apars' -> (f, a) :: comb fpars' apars' | [], _ -> - if apars <> [] then ( + if not (List.is_empty apars) then ( let str = "more actual pars than formal pars in fun call (" ^ string_of_int (List.length actual_params) @@ -1186,11 +1186,11 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop let missing_sigma_objc_class = List.filter ~f:(fun hp -> hpred_missing_objc_class hp) missing_sigma in - if missing_fld_objc_class <> [] then ( + if not (List.is_empty missing_fld_objc_class) then ( L.d_strln "Objective-C missing_fld not empty: adding it to current tenv..." ; add_missing_field_to_tenv ~missing_sigma:false exe_env tenv callee_pname missing_fld_objc_class callee_summary ) ; - if missing_sigma_objc_class <> [] then ( + if not (List.is_empty missing_sigma_objc_class) then ( L.d_strln "Objective-C missing_sigma not empty: adding it to current tenv..." ; add_missing_field_to_tenv ~missing_sigma:true exe_env tenv callee_pname missing_sigma_objc_class callee_summary ) ; @@ -1242,10 +1242,12 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop Invalid_res (Dereference_error (deref_error, desc, pjoin)) | None -> let split = do_split () in - if (not !BiabductionConfig.footprint) && split.missing_sigma <> [] then ( + if (not !BiabductionConfig.footprint) && not (List.is_empty split.missing_sigma) then ( L.d_strln "Implication error: missing_sigma not empty in re-execution" ; Invalid_res Missing_sigma_not_empty ) - else if (not !BiabductionConfig.footprint) && missing_fld_not_objc_class <> [] then ( + else if + (not !BiabductionConfig.footprint) && not (List.is_empty missing_fld_not_objc_class) + then ( L.d_strln "Implication error: missing_fld not empty in re-execution" ; Invalid_res Missing_fld_not_empty ) else report_valid_res split ) @@ -1305,7 +1307,7 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re List.map ~f:(function Valid_res _ -> assert false | Invalid_res ir -> ir) invalid_res0 in let valid_res_miss_pi, valid_res_no_miss_pi = - List.partition_tf ~f:(fun vr -> vr.vr_pi <> []) valid_res + List.partition_tf ~f:(fun vr -> not (List.is_empty vr.vr_pi)) valid_res in let _, valid_res_cons_pre_missing = List.partition_tf ~f:(fun vr -> vr.incons_pre_missing) valid_res @@ -1402,7 +1404,7 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re List.map ~f:(fun (p, path) -> (prop_pure_to_footprint tenv p, path)) (List.concat_map ~f:process_valid_res valid_res) - else if valid_res_no_miss_pi <> [] then + else if not (List.is_empty valid_res_no_miss_pi) then List.concat_map ~f:(fun vr -> vr.vr_cons_res) valid_res_no_miss_pi else if List.is_empty valid_res_miss_pi then raise (Exceptions.Precondition_not_met (call_desc None, __POS__)) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 5cc4265f1..61fd07abe 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -67,7 +67,7 @@ module SymLinear = struct let le_one_pair s v1_opt v2_opt = let v1 = NonZeroInt.opt_to_big_int v1_opt in let v2 = NonZeroInt.opt_to_big_int v2_opt in - Z.(equal v1 v2) || (Symb.Symbol.is_unsigned s && v1 <= v2) + Z.(equal v1 v2) || (Symb.Symbol.is_unsigned s && Z.leq v1 v2) in M.for_all2 ~f:le_one_pair x y @@ -186,7 +186,7 @@ module SymLinear = struct match prev_opt with | Some (prev_coeff, prev_symb) when Symb.Symbol.paths_equal prev_symb symb - && NonZeroInt.is_positive coeff <> NonZeroInt.is_positive prev_coeff -> + && Bool.(NonZeroInt.is_positive coeff <> NonZeroInt.is_positive prev_coeff) -> let add_coeff = (if NonZeroInt.is_positive coeff then NonZeroInt.max else NonZeroInt.min) prev_coeff (NonZeroInt.( ~- ) coeff) @@ -384,7 +384,7 @@ module Bound = struct let mk_MinMax (c, sign, m, d, s) = - if Symb.Symbol.is_unsigned s && Z.(d <= zero) then + if Symb.Symbol.is_unsigned s && Z.(leq d zero) then match m with | Min -> of_big_int (Sign.eval_big_int sign c d) @@ -486,7 +486,7 @@ module Bound = struct let le_minmax_by_int x y = match (big_int_ub_of_minmax x, big_int_lb_of_minmax y) with | Some n, Some m -> - n <= m + Z.leq n m | _, _ -> false @@ -508,7 +508,7 @@ module Bound = struct | MultB _, _ | _, MultB _ -> false | Linear (c0, x0), Linear (c1, x1) -> - c0 <= c1 && SymLinear.le x0 x1 + Z.leq c0 c1 && SymLinear.le x0 x1 | MinMax _, MinMax _ when le_minmax_by_int x y -> true | MinMax (c1, (Plus as sign), Min, d1, s1), MinMax (c2, Plus, Min, d2, s2) diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml index d5a965a92..ff8452a20 100644 --- a/infer/src/bufferoverrun/ints.ml +++ b/infer/src/bufferoverrun/ints.ml @@ -28,9 +28,9 @@ module NonZeroInt = struct let is_multiple m d = Z.(equal (m mod d) zero) - let is_negative x = Z.(x < zero) + let is_negative x = Z.(lt x zero) - let is_positive x = Z.(x > zero) + let is_positive x = Z.(gt x zero) let ( ~- ) = Z.( ~- ) @@ -59,7 +59,7 @@ module NonNegativeInt = struct let is_one = Z.equal one - let of_big_int i = if Z.(i < zero) then None else Some i + let of_big_int i = if Z.(lt i zero) then None else Some i let of_int_exn i = assert (i >= 0) ; @@ -67,13 +67,13 @@ module NonNegativeInt = struct let of_big_int_exn i = - assert (Z.(i >= zero)) ; + assert (Z.(geq i zero)) ; i let to_int_exn = Z.to_int - let leq ~lhs ~rhs = lhs <= rhs + let leq ~lhs ~rhs = Z.leq lhs rhs let succ = Z.succ @@ -91,7 +91,7 @@ module PositiveInt = struct let one = Z.one - let of_big_int i = if Z.(i <= zero) then None else Some i + let of_big_int i = if Z.(leq i zero) then None else Some i let succ = Z.succ @@ -101,7 +101,7 @@ module PositiveInt = struct let pp_exponent f i = let rec aux f i = - if not Z.(i <= zero) then ( + if not Z.(leq i zero) then ( let d, r = Z.ediv_rem i ten in aux f d ; F.pp_print_string f exponent_chars.(Z.to_int r) ) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5b4bff8c8..1430cc457 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -330,7 +330,7 @@ module ItvPure = struct match get_const y with | Some n when Z.(leq n zero) -> x - | Some n when Z.(n >= of_int 64) -> + | Some n when Z.(geq n (of_int 64)) -> zero | Some n -> ( match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top ) diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index e3b6b833c..4adb4ac23 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -397,11 +397,11 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct else ((s, PositiveInt.one), last :: others) in let pp_coeff fmt (c : NonNegativeInt.t) = - if Z.((c :> Z.t) > one) then + if Z.(gt (c :> Z.t) one) then F.fprintf fmt "%a %s " NonNegativeInt.pp c SpecialChars.dot_operator in let pp_exp fmt (e : PositiveInt.t) = - if Z.((e :> Z.t) > one) then PositiveInt.pp_exponent fmt e + if Z.(gt (e :> Z.t) one) then PositiveInt.pp_exponent fmt e in let pp_magic_parentheses pp fmt x = let s = F.asprintf "%a" pp x in diff --git a/infer/src/checkers/RequiredProps.ml b/infer/src/checkers/RequiredProps.ml index 0a11d8090..a9f0cb802 100644 --- a/infer/src/checkers/RequiredProps.ml +++ b/infer/src/checkers/RequiredProps.ml @@ -182,7 +182,7 @@ let should_report proc_desc tenv = let pname = Procdesc.get_proc_name proc_desc in (not (is_litho_function pname)) && (not (is_component_build_method pname tenv)) - && Procdesc.get_access proc_desc <> PredSymb.Private + && not (PredSymb.equal_access (Procdesc.get_access proc_desc) Private) let report astate tenv summary = diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 65d9fcea7..f77e612c7 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -117,10 +117,16 @@ module MakeDF (St : DFStateType) : DF with type state = St.t = struct in let succ_nodes = Procdesc.Node.get_succs node in let exn_nodes = Procdesc.Node.get_exn node in - if throws <> Throws then - List.iter ~f:(fun s -> List.iter ~f:(propagate_to_dest s) succ_nodes) states_succ ; - if throws <> DoesNotThrow then - List.iter ~f:(fun s -> List.iter ~f:(propagate_to_dest s) exn_nodes) states_exn ; + ( match throws with + | DoesNotThrow | DontKnow -> + List.iter ~f:(fun s -> List.iter ~f:(propagate_to_dest s) succ_nodes) states_succ + | Throws -> + () ) ; + ( match throws with + | Throws | DontKnow -> + List.iter ~f:(fun s -> List.iter ~f:(propagate_to_dest s) exn_nodes) states_exn + | DoesNotThrow -> + () ) ; H.replace t.post_states node states_succ ; H.replace t.exn_states node states_exn diff --git a/infer/src/clang/ClangWrapper.ml b/infer/src/clang/ClangWrapper.ml index e08c4c129..d3d2e3393 100644 --- a/infer/src/clang/ClangWrapper.ml +++ b/infer/src/clang/ClangWrapper.ml @@ -41,7 +41,10 @@ let check_for_existing_file args = Create empty file empty file and pass that to clang. This is to enable compilation to continue *) match List.hd rest with | Some arg -> - if Str.string_match clang_ignore_regex arg 0 && Sys.file_exists arg <> `Yes then ( + if + Str.string_match clang_ignore_regex arg 0 + && PolyVariantEqual.(Sys.file_exists arg <> `Yes) + then ( Unix.mkdir_p (Filename.dirname arg) ; let file = Unix.openfile ~mode:[Unix.O_CREAT; Unix.O_RDONLY] arg in Unix.close file ) diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 106a172f1..74e22b2d8 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -25,7 +25,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let get_callee_objc_method context obj_c_message_expr_info callee_ms_opt act_params = let open CContext in let selector, mc_type = CMethod_trans.get_objc_method_data obj_c_message_expr_info in - let is_instance = mc_type <> CMethod_trans.MCStatic in + let is_instance = not (CMethod_trans.equal_method_call_type mc_type MCStatic) in let objc_method_kind = Procname.ObjC_Cpp.objc_method_kind_of_bool is_instance in let method_kind = if is_instance then ClangMethodKind.OBJC_INSTANCE else ClangMethodKind.OBJC_CLASS @@ -106,7 +106,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let exec_with_node_creation ~f trans_state stmt = let res_trans = f trans_state stmt in - if res_trans.control.instrs <> [] then + if not (List.is_empty res_trans.control.instrs) then let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in let stmt_info' = {stmt_info with Clang_ast_t.si_pointer= CAst_utils.get_fresh_pointer ()} in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info' in @@ -903,14 +903,14 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let i_exp, _ = res_trans_idx.return in let array_exp = Exp.Lindex (a_exp, i_exp) in let root_nodes = - if res_trans_a.control.root_nodes <> [] then res_trans_a.control.root_nodes + if not (List.is_empty res_trans_a.control.root_nodes) then res_trans_a.control.root_nodes else res_trans_idx.control.root_nodes in let leaf_nodes = - if res_trans_idx.control.leaf_nodes <> [] then res_trans_idx.control.leaf_nodes + if not (List.is_empty res_trans_idx.control.leaf_nodes) then res_trans_idx.control.leaf_nodes else res_trans_a.control.leaf_nodes in - if res_trans_idx.control.root_nodes <> [] then + if not (List.is_empty res_trans_idx.control.root_nodes) then List.iter ~f:(fun n -> Procdesc.node_set_succs context.procdesc n ~normal:res_trans_idx.control.root_nodes @@ -1366,7 +1366,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s and add_this_instrs_if_result_non_empty res_trans this_res_trans = - if res_trans <> [] then + if not (List.is_empty res_trans) then mk_trans_result this_res_trans.return {empty_control with instrs= this_res_trans.control.instrs} :: res_trans @@ -1637,7 +1637,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s ~node_name:BinaryConditionalStmtInit stmt_info init_res_trans in let root_nodes = init_res_trans'.control.root_nodes in - if root_nodes <> [] then {op_res_trans with control= {op_res_trans.control with root_nodes}} + if not (List.is_empty root_nodes) then + {op_res_trans with control= {op_res_trans.control with root_nodes}} else op_res_trans | _ -> CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range @@ -1896,7 +1897,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s ~f:(fun n' -> Procdesc.node_set_succs context.procdesc n' ~normal:[switch_node] ~exn:[]) res_trans_cond_tmp.control.leaf_nodes ; let root_nodes = - if res_trans_cond_tmp.control.root_nodes <> [] then res_trans_cond_tmp.control.root_nodes + if not (List.is_empty res_trans_cond_tmp.control.root_nodes) then + res_trans_cond_tmp.control.root_nodes else [switch_node] in let condition_exp, _ = res_trans_cond_tmp.return in @@ -3812,7 +3814,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s | trans_stmt_fun :: trans_stmt_fun_list' -> let res_trans_s = trans_stmt_fun trans_state in let trans_state' = - if res_trans_s.control.root_nodes <> [] then + if not (List.is_empty res_trans_s.control.root_nodes) then {trans_state with succ_nodes= res_trans_s.control.root_nodes} else trans_state in diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 17cc70cf6..e459db8b0 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -165,12 +165,14 @@ let undefined_expression () = Exp.Var (Ident.create_fresh Ident.knormal) (** Collect the results of translating a list of instructions, and link up the nodes created. *) let collect_controls pdesc l = let collect_one result_rev {root_nodes; leaf_nodes; instrs; initd_exps} = - if root_nodes <> [] then + if not (List.is_empty root_nodes) then List.iter ~f:(fun n -> Procdesc.node_set_succs pdesc n ~normal:root_nodes ~exn:[]) result_rev.leaf_nodes ; - let root_nodes = if result_rev.root_nodes <> [] then result_rev.root_nodes else root_nodes in - let leaf_nodes = if leaf_nodes <> [] then leaf_nodes else result_rev.leaf_nodes in + let root_nodes = + if List.is_empty result_rev.root_nodes then root_nodes else result_rev.root_nodes + in + let leaf_nodes = if List.is_empty leaf_nodes then result_rev.leaf_nodes else leaf_nodes in { root_nodes ; leaf_nodes ; instrs= List.rev_append instrs result_rev.instrs @@ -216,7 +218,9 @@ module PriorityNode = struct (* priority_node. It returns nodes, ids, instrs that should be passed to parent *) let compute_controls_to_parent trans_state loc ~node_name stmt_info res_states_children = let res_state = collect_controls trans_state.context.procdesc res_states_children in - let create_node = own_priority_node trans_state.priority stmt_info && res_state.instrs <> [] in + let create_node = + own_priority_node trans_state.priority stmt_info && not (List.is_empty res_state.instrs) + in if create_node then ( (* We need to create a node *) let node_kind = Procdesc.Node.Stmt_node node_name in @@ -230,7 +234,9 @@ module PriorityNode = struct Procdesc.node_set_succs trans_state.context.procdesc leaf ~normal:[node] ~exn:[] ) res_state.leaf_nodes ; (* Invariant: if root_nodes is empty then the params have not created a node.*) - let root_nodes = if res_state.root_nodes <> [] then res_state.root_nodes else [node] in + let root_nodes = + if List.is_empty res_state.root_nodes then [node] else res_state.root_nodes + in {res_state with root_nodes; leaf_nodes= [node]; instrs= []} ) else (* The node is created by the parent. We just pass back nodes/leafs params *) res_state diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 8f8de0008..a7aababc2 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -851,11 +851,11 @@ let should_report_on_proc tenv procdesc = (* return true if procedure is at an abstraction boundary or reporting has been explicitly requested via @ThreadSafe in java *) RacerDModels.is_thread_safe_method proc_name tenv - || Procdesc.get_access procdesc <> PredSymb.Private + || (not (PredSymb.equal_access (Procdesc.get_access procdesc) Private)) && (not (Procname.Java.is_autogen_method java_pname)) && not (Annotations.pdesc_return_annot_ends_with procdesc Annotations.visibleForTesting) | ObjC_Cpp {kind= CPPMethod _ | CPPConstructor _ | CPPDestructor _} -> - Procdesc.get_access procdesc <> PredSymb.Private + not (PredSymb.equal_access (Procdesc.get_access procdesc) Private) | ObjC_Cpp {kind= ObjCClassMethod | ObjCInstanceMethod | ObjCInternalMethod; class_name} -> Tenv.lookup tenv class_name |> Option.exists ~f:(fun {Struct.exported_objc_methods} -> diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 771b586f8..e7864512e 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -62,7 +62,7 @@ let float_of_const_int = function None -let is_excessive_secs duration = duration >. android_anr_time_limit +let is_excessive_secs duration = Float.(duration > android_anr_time_limit) type severity = Low | Medium | High [@@deriving compare] diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 709e7877a..c3abeb183 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -570,7 +570,7 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem = let should_report pdesc = - Procdesc.get_access pdesc <> PredSymb.Private + (not (PredSymb.equal_access (Procdesc.get_access pdesc) Private)) && match Procdesc.get_proc_name pdesc with | Procname.Java java_pname -> diff --git a/infer/src/integration/Buck.ml b/infer/src/integration/Buck.ml index 27b9537bc..a34e0c3c2 100644 --- a/infer/src/integration/Buck.ml +++ b/infer/src/integration/Buck.ml @@ -232,7 +232,7 @@ let inline_argument_files buck_args = let expand_buck_arg buck_arg = if String.is_prefix ~prefix:"@" buck_arg then let file_name = String.chop_prefix_exn ~prefix:"@" buck_arg in - if Sys.file_exists file_name <> `Yes then [buck_arg] + if PolyVariantEqual.(Sys.file_exists file_name <> `Yes) then [buck_arg] (* Arguments that start with @ could mean something different than an arguments file in buck. *) else let expanded_args = diff --git a/infer/src/integration/Driver.ml b/infer/src/integration/Driver.ml index bccc131c8..4d84961db 100644 --- a/infer/src/integration/Driver.ml +++ b/infer/src/integration/Driver.ml @@ -445,7 +445,7 @@ let fail_on_issue_epilogue () = match Utils.read_file issues_json with | Ok lines -> let issues = Jsonbug_j.report_of_string @@ String.concat ~sep:"" lines in - if issues <> [] then L.exit Config.fail_on_issue_exit_code + if not (List.is_empty issues) then L.exit Config.fail_on_issue_exit_code | Error error -> L.internal_error "Failed to read report file '%s': %s@." issues_json error ; () diff --git a/infer/src/istd/PolyVariantEqual.ml b/infer/src/istd/PolyVariantEqual.ml index 82f6ee5b1..1bd41a299 100644 --- a/infer/src/istd/PolyVariantEqual.ml +++ b/infer/src/istd/PolyVariantEqual.ml @@ -8,3 +8,5 @@ open! Core let ( = ) (v1 : [> ]) (v2 : [> ]) = Poly.equal v1 v2 + +let ( <> ) (v1 : [> ]) (v2 : [> ]) = not (v1 = v2) diff --git a/infer/src/istd/PolyVariantEqual.mli b/infer/src/istd/PolyVariantEqual.mli index 9f397b2b9..e559cfb41 100644 --- a/infer/src/istd/PolyVariantEqual.mli +++ b/infer/src/istd/PolyVariantEqual.mli @@ -11,3 +11,6 @@ open! Core val ( = ) : ([> ] as 'a) -> 'a -> bool (** Equality for polymorphic variants *) + +val ( <> ) : ([> ] as 'a) -> 'a -> bool +(** Disequality for polymorphic variants *) diff --git a/infer/src/istd/Pp.ml b/infer/src/istd/Pp.ml index eda525c4e..b0f940e2f 100644 --- a/infer/src/istd/Pp.ml +++ b/infer/src/istd/Pp.ml @@ -106,7 +106,7 @@ let html_with_color color pp f x = let color_wrapper pe ppf x ~f = match pe.kind with - | HTML when pe.cmap_norm (Obj.repr x) <> pe.color -> + | HTML when not (equal_color (pe.cmap_norm (Obj.repr x)) pe.color) -> let color = pe.cmap_norm (Obj.repr x) in let pe' = if equal_color color Red then diff --git a/infer/src/istd/StatisticsToolbox.ml b/infer/src/istd/StatisticsToolbox.ml index e4efcee8c..1e31a860d 100644 --- a/infer/src/istd/StatisticsToolbox.ml +++ b/infer/src/istd/StatisticsToolbox.ml @@ -26,17 +26,18 @@ let compute_statistics values = | [] -> None | _ :: _ as values -> + let open Float in let num_elements = List.length values in let sum = List.fold ~f:(fun acc v -> acc +. v) ~init:0.0 values in let average = sum /. float_of_int num_elements in let values_arr = Array.of_list values in Array.sort - ~compare:(fun a b -> if Float.equal a b then 0 else if a -. b < 0.0 then -1 else 1) + ~compare:(fun a b -> if equal a b then 0 else if a -. b < 0.0 then -1 else 1) values_arr ; let percentile pct = assert (pct >= 0.0 && pct <= 1.0) ; - assert (num_elements > 0) ; - let max_index = num_elements - 1 in + assert (Int.(num_elements > 0)) ; + let max_index = Int.(num_elements - 1) in let pct_index = float_of_int max_index *. pct in let low_index = int_of_float (Stdlib.floor pct_index) in let high_index = int_of_float (Stdlib.ceil pct_index) in diff --git a/infer/src/nullsafe/AnnotatedSignature.ml b/infer/src/nullsafe/AnnotatedSignature.ml index 3d920074d..3f5171cea 100644 --- a/infer/src/nullsafe/AnnotatedSignature.ml +++ b/infer/src/nullsafe/AnnotatedSignature.ml @@ -124,7 +124,7 @@ let param_has_annot predicate pvar ann_sig = let pp proc_name fmt annotated_signature = - let pp_ia fmt ia = if ia <> [] then F.fprintf fmt "%a " Annot.Item.pp ia in + let pp_ia fmt ia = if not (List.is_empty ia) then F.fprintf fmt "%a " Annot.Item.pp ia in let pp_annotated_param fmt {mangled; param_annotation_deprecated; param_annotated_type} = F.fprintf fmt " %a%a %a" pp_ia param_annotation_deprecated AnnotatedType.pp param_annotated_type Mangled.pp mangled diff --git a/infer/src/nullsafe/Initializers.ml b/infer/src/nullsafe/Initializers.ml index 94543d9f1..3c08e2c99 100644 --- a/infer/src/nullsafe/Initializers.ml +++ b/infer/src/nullsafe/Initializers.ml @@ -62,7 +62,7 @@ let final_typestates initializers_current_class tenv typecheck_proc = List.filter ~f:(fun (pn, _) -> not (Procname.Set.mem pn !seen)) initializers_new in mark_seen initializers_new' ; - if initializers_new' <> [] then fixpoint initializers_new' + if not (List.is_empty initializers_new') then fixpoint initializers_new' in mark_seen initializers_base_case ; fixpoint initializers_base_case ; !res in diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index e35d03a6d..a8736843e 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -66,7 +66,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct String.equal (PatternMatch.get_type_name ret_annotated_type.typ) "java.lang.Void" in State.set_node exit_node ; - if checks.TypeCheck.check_ret_type <> [] then + if not (List.is_empty checks.TypeCheck.check_ret_type) then List.iter ~f:(fun f -> f curr_pname curr_pdesc ret_annotated_type.typ typ_found_opt loc) checks.TypeCheck.check_ret_type ; diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 76f328dd7..a8cad4878 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -267,7 +267,7 @@ let convert_complex_exp_to_pvar tenv idenv curr_pname in let default = (exp, typestate) in match exp with - | Exp.Var id when Errdesc.find_normal_variable_funcall node id <> None -> + | Exp.Var id when Option.is_some (Errdesc.find_normal_variable_funcall node id) -> ( funcall_exp_to_original_pvar_exp tenv curr_pname typestate exp ~is_assignment ~call_node:node ~node id , typestate ) @@ -1180,7 +1180,7 @@ let typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canon let has_exceptions = match callee_attributes_opt with | Some callee_attributes -> - callee_attributes.ProcAttributes.exceptions <> [] + not (List.is_empty callee_attributes.ProcAttributes.exceptions) | None -> false in diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 6ea1c3859..bea235686 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -868,7 +868,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct | Some access_tree -> Payload.update_summary (make_summary proc_data access_tree) summary | None -> - if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then ( + if not (List.is_empty (Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc))) then ( L.internal_error "Couldn't compute post for %a. Broken CFG suspected" Procname.pp pname ; summary ) else summary diff --git a/infer/src/scripts/checkCopyright.ml b/infer/src/scripts/checkCopyright.ml index 238f30597..e692b7eca 100644 --- a/infer/src/scripts/checkCopyright.ml +++ b/infer/src/scripts/checkCopyright.ml @@ -274,7 +274,9 @@ let output_diff ~fname lines ?notice_range ?(monoidics = false) ?(ropas = false) for i = 0 to copy_lines_before do F.fprintf fmt "%s\n" lines.(i) done ; - if starts_with_newline com_style && copy_lines_before > 0 && lines.(copy_lines_before - 1) <> "" + if + starts_with_newline com_style && copy_lines_before > 0 + && not (String.is_empty lines.(copy_lines_before - 1)) then F.fprintf fmt "@\n" ; pp_copyright ~monoidics ~ropas com_style fmt ; for i = copy_lines_after to Array.length lines - 1 do diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index b95c314bd..79571028f 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -17,7 +17,7 @@ module MockTraceDomain = struct let top = singleton top_str let singleton e = - assert (e <> top_str) ; + assert (String.(e <> top_str)) ; singleton e diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 232e2a72a..3ab84b715 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -262,7 +262,7 @@ struct F.asprintf "%a" pp_state post with Caml.Not_found -> "_|_" in - if inv_str <> post_str then + if not (String.equal inv_str post_str) then let error_msg = F.fprintf F.str_formatter "> Expected state %s at invariant %d, but found state %s" inv_str inv_label post_str