From 32146523ca4368449fba886c9e71a002906ad277 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 4 Aug 2016 04:00:58 -0700 Subject: [PATCH] Enable warning: Unexpected documentation comment Summary: Enable warning 50 (Unexpected documentation comment) and fix all current reports. Reviewed By: jvillard Differential Revision: D3653660 fbshipit-source-id: bfd36b9 --- infer/.merlin | 2 +- infer/src/Makefile | 4 +- infer/src/backend/CommandLineOption.ml | 14 +++--- infer/src/backend/SymOp.ml | 16 +++---- infer/src/backend/SymOp.mli | 8 ++-- infer/src/backend/abs.ml | 43 +++++++++--------- infer/src/backend/builtin.ml | 10 ++--- infer/src/backend/callbacks.ml | 2 +- infer/src/backend/config.ml | 46 ++++++++++---------- infer/src/backend/crashcontext.ml | 2 +- infer/src/backend/exceptions.ml | 10 +++-- infer/src/backend/exceptions.mli | 12 ++--- infer/src/backend/infer.ml | 16 +++---- infer/src/backend/inferanalyze.ml | 4 +- infer/src/backend/inferprint.ml | 2 +- infer/src/backend/interproc.ml | 8 ++-- infer/src/backend/io_infer.mli | 3 ++ infer/src/backend/logging.ml | 2 +- infer/src/backend/mergeCapture.ml | 2 +- infer/src/backend/modelBuiltins.mli | 2 + infer/src/backend/ondemand.ml | 2 +- infer/src/backend/paths.ml | 26 ++++++----- infer/src/backend/preanal.ml | 8 ++-- infer/src/backend/prop.ml | 15 ++++--- infer/src/backend/prop.mli | 2 + infer/src/backend/prover.ml | 14 +++--- infer/src/backend/rearrange.ml | 4 +- infer/src/backend/rearrange.mli | 5 +-- infer/src/backend/specs.ml | 10 ++++- infer/src/backend/specs.mli | 24 +++++----- infer/src/backend/state.ml | 18 ++++---- infer/src/backend/symExec.ml | 8 ++-- infer/src/backend/tabulation.ml | 24 +++++----- infer/src/backend/timeout.ml | 4 +- infer/src/backend/utils.ml | 4 +- infer/src/backend/utils.mli | 7 ++- infer/src/checkers/BoundedCallTree.ml | 15 +++---- infer/src/checkers/checkTraceCallSequence.ml | 4 +- infer/src/checkers/checkers.ml | 6 +-- infer/src/checkers/checkers.mli | 1 + infer/src/checkers/dataflow.ml | 14 ++++-- infer/src/checkers/dataflow.mli | 15 +++++-- infer/src/checkers/procCfg.ml | 12 +++++ infer/src/checkers/procCfg.mli | 12 +++++ infer/src/checkers/repeatedCallsChecker.ml | 2 +- infer/src/clang/cFrontend_config.mli | 2 + infer/src/clang/cMethod_trans.ml | 13 +++--- infer/src/clang/cMethod_trans.mli | 9 ++-- infer/src/clang/cTrans.ml | 6 +-- infer/src/clang/cTrans.mli | 9 ++-- infer/src/clang/cTrans_utils.ml | 4 +- infer/src/clang/cTrans_utils.mli | 29 ++++++------ infer/src/clang/objcInterface_decl.mli | 5 +-- infer/src/eradicate/eradicate.ml | 10 ++--- infer/src/eradicate/typeCheck.ml | 26 +++++------ infer/src/eradicate/typeState.ml | 5 ++- infer/src/eradicate/typeState.mli | 5 ++- infer/src/java/jTransType.ml | 1 + infer/src/llvm/lTrans.ml | 2 +- 59 files changed, 324 insertions(+), 266 deletions(-) diff --git a/infer/.merlin b/infer/.merlin index 46e27193d..fcc119eea 100644 --- a/infer/.merlin +++ b/infer/.merlin @@ -11,4 +11,4 @@ PKG unix PKG yojson PKG zip FLG -principal -safe-string -short-paths -strict-formats -strict-sequence -FLG -w +a-4-9-40-41-42-45-48-50 +FLG -w +a-4-9-40-41-42-45-48 diff --git a/infer/src/Makefile b/infer/src/Makefile index 147c88826..076208619 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -19,7 +19,7 @@ ATDGEN_SUFFIXES = _t.ml _t.mli _j.ml _j.mli #### ocamlbuild options #### -OCAML_FATAL_WARNINGS = +5+6+8+10+11+12+18+19+20+26+29+27+32+33+34+35+37+38+39 +OCAML_FATAL_WARNINGS = +5+6+8+10+11+12+18+19+20+26+29+27+32+33+34+35+37+38+39+50 OCAMLBUILD_OPTIONS = \ -r \ @@ -29,7 +29,7 @@ OCAMLBUILD_OPTIONS = \ -cflags -principal \ -cflags -strict-formats \ -cflags -strict-sequence \ - -cflags -w,$(OCAML_FATAL_WARNINGS)-4-9-40-41-42-45-48-50 \ + -cflags -w,$(OCAML_FATAL_WARNINGS)-4-9-40-41-42-45-48 \ -tag-line "<*{clang/clang_ast_*,backend/jsonbug_*,checkers/stacktree_*}>: warn(-27-32-35-39)" \ -pkgs atdgen,extlib,oUnit,str,unix,yojson,zip diff --git a/infer/src/backend/CommandLineOption.ml b/infer/src/backend/CommandLineOption.ml index d49f20e9e..57d584ead 100644 --- a/infer/src/backend/CommandLineOption.ml +++ b/infer/src/backend/CommandLineOption.ml @@ -15,8 +15,8 @@ module F = Format module YBU = Yojson.Basic.Util -(* Each command line option may appear in the --help list of any executable, these tags are used to - specify which executables for which an option will be documented. *) +(** Each command line option may appear in the --help list of any executable, these tags are used to + specify which executables for which an option will be documented. *) type exe = Analyze | Clang | Java | Llvm | Print | StatsAggregator | Toplevel let exes = [ @@ -122,7 +122,7 @@ let full_desc_list = ref [] let exe_desc_lists = IList.map (fun (_, exe) -> (exe, ref [])) exes -(* add desc to all desc_lists for the purposes of parsing, include desc in --help only for exes *) +(** add desc to all desc_lists for the purposes of parsing, include desc in --help only for exes *) let add exes desc = full_desc_list := desc :: !full_desc_list ; IList.iter (fun (exe, desc_list) -> @@ -312,12 +312,12 @@ let mk_set_from_json ~default ~default_to_string ~f ~decode_json:(fun json -> [dashdash long; Yojson.Basic.to_string json]) ~mk_spec:(fun set -> Arg.String set) -(* A ref to a function used during argument parsing to process anonymous arguments. By default, - anonymous arguments are rejected. *) +(** A ref to a function used during argument parsing to process anonymous arguments. By default, + anonymous arguments are rejected. *) let anon_fun = ref (fun arg -> raise (Arg.Bad ("unexpected anonymous argument: " ^ arg))) -(* Clients declare that anonymous arguments are acceptable by calling [mk_anon], which returns a ref - storing the anonymous arguments. *) +(** Clients declare that anonymous arguments are acceptable by calling [mk_anon], which returns a + ref storing the anonymous arguments. *) let mk_anon () = let anon = ref [] in anon_fun := (fun arg -> anon := arg :: !anon) ; diff --git a/infer/src/backend/SymOp.ml b/infer/src/backend/SymOp.ml index f01d4c8d0..8ae287e9d 100644 --- a/infer/src/backend/SymOp.ml +++ b/infer/src/backend/SymOp.ml @@ -16,10 +16,10 @@ module F = Format type failure_kind = - | FKtimeout (* max time exceeded *) - | FKsymops_timeout of int (* max symop's exceeded *) - | FKrecursion_timeout of int (* max recursion level exceeded *) - | FKcrash of string (* uncaught exception or failed assertion *) + | FKtimeout (** max time exceeded *) + | FKsymops_timeout of int (** max symop's exceeded *) + | FKrecursion_timeout of int (** max recursion level exceeded *) + | FKcrash of string (** uncaught exception or failed assertion *) (** failure that prevented analysis from finishing *) exception Analysis_failure_exe of failure_kind @@ -68,19 +68,19 @@ let get_timeout_seconds () = !timeout_seconds (** Internal state of the module *) type t = { - (** Only throw timeout exception when alarm is active *) mutable alarm_active : bool; + (** Only throw timeout exception when alarm is active *) - (** last wallclock set by an alarm, if any *) mutable last_wallclock : float option; + (** last wallclock set by an alarm, if any *) - (** Number of symop's *) mutable symop_count : int; + (** Number of symop's *) + symop_total : int ref; (** Counter for the total number of symop's. The new state created when save_state is called shares this counter if keep_symop_total is true. Otherwise, a new counter is created. *) - symop_total : int ref; } let initial () : t = diff --git a/infer/src/backend/SymOp.mli b/infer/src/backend/SymOp.mli index dc07dd793..be7aadfe0 100644 --- a/infer/src/backend/SymOp.mli +++ b/infer/src/backend/SymOp.mli @@ -57,10 +57,10 @@ val unset_wallclock_alarm : unit -> unit type failure_kind = - | FKtimeout (* max time exceeded *) - | FKsymops_timeout of int (* max symop's exceeded *) - | FKrecursion_timeout of int (* max recursion level exceeded *) - | FKcrash of string (* uncaught exception or failed assertion *) + | FKtimeout (** max time exceeded *) + | FKsymops_timeout of int (** max symop's exceeded *) + | FKrecursion_timeout of int (** max recursion level exceeded *) + | FKcrash of string (** uncaught exception or failed assertion *) (** Timeout exception *) exception Analysis_failure_exe of failure_kind diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 9084c0286..b8001a7b6 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -764,7 +764,7 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) = let pi_filtered = let sigma = Prop.get_sigma p in let fav_sigma = Prop.sigma_fav sigma in - let fav_nonpure = Prop.prop_fav_nonpure p in (** vars in current and footprint sigma *) + let fav_nonpure = Prop.prop_fav_nonpure p in (* vars in current and footprint sigma *) let filter atom = let fav' = Sil.atom_fav atom in Sil.fav_for_all fav' (fun id -> @@ -801,7 +801,7 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) = else eprop' in Prop.normalize eprop'' -(* Collect symbolic garbage from pi and sigma *) +(** Collect symbolic garbage from pi and sigma *) let abstract_gc p = let pi = Prop.get_pi p in let p_without_pi = Prop.normalize (Prop.replace_pi [] p) in @@ -825,6 +825,7 @@ let abstract_gc p = | Some iter -> Prop.prop_iter_to_prop (Prop.prop_iter_gc_fields iter) module IdMap = Map.Make (Ident) (** maps from identifiers *) + module HpredSet = Set.Make(struct type t = Sil.hpred @@ -889,9 +890,9 @@ let get_cycle root prop = ^(Ident.fieldname_to_string f)^", "^(Sil.exp_to_string e')^")") | _ -> ()) cyc; L.d_strln "") in - (* perform a dfs of a graph stopping when e_root is reached. *) - (* Returns a pair (path, bool) where path is a list of edges ((e1,type_e1),f,e2) *) - (* describing the path to e_root and bool is true if e_root is reached. *) + (* Perform a dfs of a graph stopping when e_root is reached. + Returns a pair (path, bool) where path is a list of edges ((e1,type_e1),f,e2) + describing the path to e_root and bool is true if e_root is reached. *) let rec dfs e_root et_src path el visited = match el with | [] -> path, false @@ -924,9 +925,9 @@ let get_cycle root prop = | _ -> L.d_strln "Root exp is not an allocated object. No cycle found"; [] -(* Check whether the hidden counter field of a struct representing an *) -(* objective-c object is positive, and whether the leak is part of the *) -(* specified buckets. In the positive case, it returns the bucket *) +(** Check whether the hidden counter field of a struct representing an objective-c object is + positive, and whether the leak is part of the specified buckets. In the positive case, it + returns the bucket *) let should_raise_objc_leak hpred = match hpred with | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Const.Cint i)), _)):: _, _), @@ -969,10 +970,10 @@ let get_var_retain_cycle _prop = | _ -> (match find_block e with | Some blk -> [((sexp blk, t), f, e')] | _ -> [((sexp (Sil.Sizeof (t, None, Subtype.exact)), t), f, e')]) in - (* returns the pvars of the first cycle we find in sigma. *) - (* This is an heuristic that works if there is one cycle. *) - (* In case there are more than one cycle we may return not necessarily*) - (* the one we are looking for. *) + (* returns the pvars of the first cycle we find in sigma. + This is an heuristic that works if there is one cycle. + In case there are more than one cycle we may return not necessarily + the one we are looking for. *) let rec do_sigma sigma_todo = match sigma_todo with | [] -> [] @@ -989,8 +990,8 @@ let remove_opt _prop = | 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 *) +(** Checks if cycle has fields (derived from a property or directly defined as ivar) with attributes + weak/unsafe_unretained/assing *) let cycle_has_weak_or_unretained_or_assign_field cycle = (* returns items annotation for field fn in struct t *) let get_item_annotation t fn = @@ -1129,9 +1130,9 @@ let check_junk ?original_prop pname tenv prop = let ignore_resource, exn = (match alloc_attribute, resource with | Some _, Sil.Rmemory Sil.Mobjc when (hpred_in_cycle hpred) -> - (* When there is a cycle in objc we ignore it *) - (* only if it's empty or it has weak or unsafe_unretained fields. *) - (* Otherwise we report a retain cycle. *) + (* When there is a cycle in objc we ignore it + only if it's empty or it has weak or unsafe_unretained fields. + Otherwise we report a retain cycle. *) let cycle = get_var_retain_cycle (remove_opt original_prop) in let ignore_cycle = (IList.length cycle = 0) || @@ -1146,9 +1147,9 @@ let check_junk ?original_prop pname tenv prop = | Some _, Sil.Rfile -> false, exn_leak | Some _, Sil.Rlock -> false, exn_leak | _ when hpred_in_cycle hpred && Sil.has_objc_ref_counter hpred -> - (* When its a cycle and the object has a ref counter then *) - (* we have a retain cycle. Objc object may not have the *) - (* Sil.Mobjc qualifier when added in footprint doing abduction *) + (* When it's a cycle and the object has a ref counter then + we have a retain cycle. Objc object may not have the + Sil.Mobjc qualifier when added in footprint doing abduction *) let cycle = get_var_retain_cycle (remove_opt original_prop) in IList.length cycle = 0, exn_retain_cycle cycle | _ -> !Config.curr_language = Config.Java, exn_leak) in @@ -1208,7 +1209,7 @@ let abstract_prop pname tenv ~(rename_primed: bool) ~(from_abstract_footprint: b then pure_abs_p else abstract_pure_part ~from_abstract_footprint: from_abstract_footprint (Absarray.abstract_array_check pure_abs_p) in let abs_p = abs_rules_apply tenv array_abs_p in - let abs_p = abstract_gc abs_p in (** abstraction might enable more gc *) + let abs_p = abstract_gc abs_p in (* abstraction might enable more gc *) let abs_p = check_junk ~original_prop: (Some(p)) pname tenv abs_p in let ren_abs_p = if rename_primed diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml index 7a86f1ca4..d6da76731 100644 --- a/infer/src/backend/builtin.ml +++ b/infer/src/backend/builtin.ml @@ -27,25 +27,25 @@ type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list type t = args -> ret_typ -(* builtin function names for which we do symbolic execution *) +(** builtin function names for which we do symbolic execution *) let builtin_functions = Procname.Hash.create 4 -(* Check if the function is a builtin *) +(** check if the function is a builtin *) let is_registered name = Procname.Hash.mem builtin_functions name -(* get the symbolic execution handler associated to the builtin function name *) +(** get the symbolic execution handler associated to the builtin function name *) let get name : t = try Procname.Hash.find builtin_functions name with Not_found -> assert false -(* register a builtin function name and symbolic execution handler *) +(** register a builtin function name and symbolic execution handler *) let register proc_name_str (sym_exe_fun: t) = let proc_name = Procname.from_string_c_fun proc_name_str in Procname.Hash.replace builtin_functions proc_name sym_exe_fun; proc_name -(* register a builtin [Procname.t] and symbolic execution handler *) +(** register a builtin [Procname.t] and symbolic execution handler *) let register_procname proc_name (sym_exe_fun: t) = Procname.Hash.replace builtin_functions proc_name sym_exe_fun diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 0feb3d766..4d4f8d2c1 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -118,7 +118,7 @@ let iterate_cluster_callbacks all_procs exe_env proc_names = (fun (idenv, tenv, proc_name, proc_desc, _) -> (idenv, tenv, proc_name, proc_desc)) procedure_definitions in - (** Procedures matching the given language or all if no language is specified. *) + (* Procedures matching the given language or all if no language is specified. *) let relevant_procedures language_opt = Option.map_default (fun l -> IList.filter (fun p -> l = get_language p) proc_names) diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 3717fa8d1..84e4cae92 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -344,8 +344,8 @@ let patterns_of_json_with_key json_key json = (** Command Line options *) -(* The working directory of the initial invocation of infer, to which paths passed as command line - options are relative. *) +(** The working directory of the initial invocation of infer, to which paths passed as command line + options are relative. *) let init_work_dir = try Sys.getenv "INFER_CWD" @@ -368,8 +368,8 @@ let init_work_dir = Unix.putenv "INFER_CWD" cwd ; cwd -(* Resolve relative paths passed as command line options, i.e., with respect to the working - directory of the initial invocation of infer. *) +(** Resolve relative paths passed as command line options, i.e., with respect to the working + directory of the initial invocation of infer. *) let resolve path = if Filename.is_relative path then init_work_dir // path @@ -405,31 +405,31 @@ let inferconfig_path = (* Proceed to declare and parse the remaining options *) -(** HOWTO define a new command line and config file option. +(* HOWTO define a new command line and config file option. - 1. Add an entry in the following let...and...and... binding. See the documentation in - [CommandLineOption.mli], and use the existing options as a guide. Preferably the identifer - and long option name are the same modulo underscores versus hyphens. + 1. Add an entry in the following let...and...and... binding. See the documentation in + [CommandLineOption.mli], and use the existing options as a guide. Preferably the identifer + and long option name are the same modulo underscores versus hyphens. - E.g. [and new_option = CLOpt.mk_bool ~long:"new-option"] + E.g. [and new_option = CLOpt.mk_bool ~long:"new-option"] - 2. Add a line to the [Freeze initialized configuration values] section below. + 2. Add a line to the [Freeze initialized configuration values] section below. - E.g. [and new_option = !new_option] + E.g. [and new_option = !new_option] - 3. Add a line to [config.mli]. + 3. Add a line to [config.mli]. - E.g. [val new_option : bool] + E.g. [val new_option : bool] - These are all in alphabetical order as much as possible. + These are all in alphabetical order as much as possible. - The references representing the command line options are defined in a single - simultaneous let...and...and... binding in order to allow the type-checker to catch - uses of one reference in code for another. This avoids being sensitive to - initialization-order and unintended dependence on the order in which options appear on - the command line. For cases where order-dependence is desired, the interacting options - can be defined together sharing a reference. See debug and specs_library below for two - different examples. *) + The references representing the command line options are defined in a single + simultaneous let...and...and... binding in order to allow the type-checker to catch + uses of one reference in code for another. This avoids being sensitive to + initialization-order and unintended dependence on the order in which options appear on + the command line. For cases where order-dependence is desired, the interacting options + can be defined together sharing a reference. See debug and specs_library below for two + different examples. *) let anon_args = CLOpt.mk_anon () @@ -633,12 +633,10 @@ and cxx_experimental = "Analyze C++ methods, still experimental" and debug, print_types, write_dotty = - (** flag: if true print full type info *) let print_types = CLOpt.mk_bool ~deprecated:["print_types"] ~long:"print-types" ~default:(CLOpt.current_exe = CLOpt.Clang) "Print types in symbolic heaps" - (** flag: if true write dot files in db dir*) and write_dotty = CLOpt.mk_bool ~deprecated:["dotty"] ~long:"write-dotty" "Produce dotty files in the results directory" @@ -680,7 +678,6 @@ and enable_checks = (** command line option to activate the eradicate checker. *) and checkers, eradicate, crashcontext = - (** command line option: if true, run the analysis in checker mode *) let checkers = CLOpt.mk_bool ~deprecated:["checkers"] ~long:"checkers" "Run only the checkers instead of the full analysis" @@ -1306,6 +1303,7 @@ and bugs_xml = !bugs_xml and changed_files_index = !changed_files_index and calls_csv = !calls_csv and checkers = !checkers + (** should the checkers be run? *) and checkers_enabled = not (!eradicate || !crashcontext) and clang_include_to_override = !clang_include_to_override diff --git a/infer/src/backend/crashcontext.ml b/infer/src/backend/crashcontext.ml index dfa610fbe..abb0f8233 100644 --- a/infer/src/backend/crashcontext.ml +++ b/infer/src/backend/crashcontext.ml @@ -53,7 +53,7 @@ let stitch_summaries stacktrace_file summary_files out_file = StringMap.empty summaries in let expand_stack_frame frame = - (** TODO: Implement k > 1 case *) + (* TODO: Implement k > 1 case *) let frame_id = frame_id_of_stackframe frame in if StringMap.exists (fun key _ -> key = frame_id) summary_map then StringMap.find frame_id summary_map diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 9801df994..a02750800 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -13,12 +13,14 @@ open! Utils module L = Logging module F = Format -type exception_visibility = (** visibility of the exception *) +(** visibility of the exception *) +type exception_visibility = | Exn_user (** always add to error log *) | Exn_developer (** only add to error log in developer mode *) | Exn_system (** never add to error log *) -type exception_severity = (** severity of bugs *) +(** severity of bugs *) +type exception_severity = | High (* high severity bug *) | Medium (* medium severity bug *) | Low (* low severity bug *) @@ -234,7 +236,7 @@ let recognize_exception exn = desc, Some ml_loc, Exn_developer, Low, None, Nocat) | Precondition_not_met (desc, ml_loc) -> (Localise.precondition_not_met, - desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) (** always a warning *) + desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) (* always a warning *) | Retain_cycle (_, _, desc, ml_loc) -> (Localise.retain_cycle, desc, Some ml_loc, Exn_user, High, None, Prover) @@ -260,7 +262,7 @@ let recognize_exception exn = (Localise.skip_function, desc, None, Exn_developer, Low, None, Nocat) | Skip_pointer_dereference (desc, ml_loc) -> (Localise.skip_pointer_dereference, - desc, Some ml_loc, Exn_user, Medium, Some Kinfo, Nocat) (** always an info *) + desc, Some ml_loc, Exn_user, Medium, Some Kinfo, Nocat) (* always an info *) | Symexec_memory_error ml_loc -> (Localise.from_string "Symexec_memory_error", Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat) diff --git a/infer/src/backend/exceptions.mli b/infer/src/backend/exceptions.mli index 7fc027899..159cf61dc 100644 --- a/infer/src/backend/exceptions.mli +++ b/infer/src/backend/exceptions.mli @@ -12,15 +12,17 @@ open! Utils (** Functions for logging and printing exceptions *) -type exception_visibility = (** visibility of the exception *) +(** visibility of the exception *) +type exception_visibility = | Exn_user (** always add to error log *) | Exn_developer (** only add to error log in developer mode *) | Exn_system (** never add to error log *) -type exception_severity = (** severity of bugs *) - | High (* high severity bug *) - | Medium (* medium severity bug *) - | Low (* low severity bug *) +(** severity of bugs *) +type exception_severity = + | High (** high severity bug *) + | Medium (** medium severity bug *) + | Low (** low severity bug *) (** kind of error/warning *) type err_kind = diff --git a/infer/src/backend/infer.ml b/infer/src/backend/infer.ml index a12f03542..a684df7a1 100644 --- a/infer/src/backend/infer.ml +++ b/infer/src/backend/infer.ml @@ -94,23 +94,21 @@ let () = ) in let pid = Unix.create_process args_py.(0) args_py Unix.stdin Unix.stdout Unix.stderr in let _, status = Unix.waitpid [] pid in - (** Collect crashcontext summaries *) + (* collect crashcontext summaries *) let analysis_is_crashcontext = match Config.analyzer with | Some Crashcontext -> true | _ -> false in if analysis_is_crashcontext then - (** Check whether this is the top-level infer process *) + (* check whether this is the top-level infer process *) let top_level_infer = - (** if the '--buck' option was passed, then this is the top level process - iff the build command starts with 'buck' *) + (* if the '--buck' option was passed, then this is the top level process iff the build command + starts with 'buck' *) if Config.buck then buck - (** otherwise, we assume javac as the build command and thus only - one process *) + (* otherwise, we assume javac as the build command and thus only one process *) else true in if top_level_infer then - (** If we are the top-level process, then find the output directory and - collect all crashcontext summaries under it in a single - crashcontext.json file *) + (* if we are the top-level process, then find the output directory and collect all + crashcontext summaries under it in a single crashcontext.json file *) let root_out_dir = if buck then begin let project_root = match Config.project_root with | Some root -> root diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index e5877d43c..55ddf26c7 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -32,13 +32,13 @@ let analyze_exe_env exe_env = let line_reader = Printer.LineReader.create () in if Config.checkers then begin - (** run the checkers only *) + (* run the checkers only *) let call_graph = Exe_env.get_cg exe_env in Callbacks.iterate_callbacks Checkers.ST.store_summary call_graph exe_env end else begin - (** run the full analysis *) + (* run the full analysis *) Interproc.do_analysis exe_env; Printer.write_all_html_files line_reader exe_env; Interproc.print_stats exe_env; diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 89fbf8829..a1fd2a842 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -352,7 +352,7 @@ module BugsCsv = struct pp "\"%d\"," node_key; pp "\"%s\"," qualifier_tag_xml; pp "\"%d\"," (get_bug_hash kind type_str procedure_id filename node_key error_desc); - pp "\"%d\"," !csv_bugs_id; (** bug id *) + pp "\"%d\"," !csv_bugs_id; (* bug id *) pp "\"%s\"," always_report; pp "\"%s\"@\n" err_advice_string; in Errlog.iter pp_row err_log diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 5984051ff..f479506db 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -252,7 +252,7 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = let propagate (wl : Worklist.t) pname is_exception (pset: Paths.PathSet.t) (curr_node: Cfg.node) = let edgeset_todo = - (** prop must be a renamed prop by the invariant preserved by PropSet *) + (* prop must be a renamed prop by the invariant preserved by PropSet *) let f prop path edgeset_curr = let exn_opt = if is_exception @@ -847,7 +847,7 @@ let initial_prop let new_formals = if add_formals then IList.map construct_decl (Cfg.Procdesc.get_formals curr_f) - else [] in (** no new formals added *) + else [] in (* no new formals added *) let prop1 = Prop.prop_reset_inst (fun inst_old -> Sil.update_inst inst_old Sil.inst_formal) @@ -1420,7 +1420,7 @@ let do_analysis exe_env = assert false in let nodes = IList.map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes pdesc) in let proc_flags = Cfg.Procdesc.get_flags pdesc in - let static_err_log = Cfg.Procdesc.get_err_log pdesc in (** err log from translation *) + let static_err_log = Cfg.Procdesc.get_err_log pdesc in (* err log from translation *) let calls = get_calls pdesc in let attributes = { (Cfg.Procdesc.get_attributes pdesc) with @@ -1573,7 +1573,7 @@ let print_stats exe_env = Exe_env.iter_files (fun fname cfg -> let proc_shadowed proc_desc = - (** return true if a proc with the same name in another module was analyzed instead *) + (* return true if a proc with the same name in another module was analyzed instead *) let proc_name = Cfg.Procdesc.get_proc_name proc_desc in Exe_env.get_source exe_env proc_name <> Some fname in print_stats_cfg proc_shadowed cfg) diff --git a/infer/src/backend/io_infer.mli b/infer/src/backend/io_infer.mli index 2427d6af6..446b4c402 100644 --- a/infer/src/backend/io_infer.mli +++ b/infer/src/backend/io_infer.mli @@ -110,13 +110,16 @@ module Xml : sig | String of string (** create a tree *) val create_tree : string -> (string * string) list -> node list -> node + (** print an xml document, if the first parameter is false on a single line without preamble *) val pp_document : bool -> Format.formatter -> node -> unit (** print the opening lines of an xml document consisting of a main tree with the given name *) val pp_open : Format.formatter -> string -> unit + (** print the closing lines of an xml document consisting of a main tree with the given name *) val pp_close : Format.formatter -> string -> unit + (** print a node between a [pp_open] and a [pp_close] *) val pp_inner_node : Format.formatter -> node -> unit end diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index 415237e67..96b7a4755 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -64,7 +64,7 @@ let delayed_actions = ref [] let printer_hook = ref (Obj.magic ()) let out_formatter, err_formatter = - (** Create a directory if it does not exist already. *) + (* Create a directory if it does not exist already. *) (* This is the same as DB.create_dir, except for logging to stderr *) let create_dir dir = try diff --git a/infer/src/backend/mergeCapture.ml b/infer/src/backend/mergeCapture.ml index e81c5a4ab..2f4717a74 100644 --- a/infer/src/backend/mergeCapture.ml +++ b/infer/src/backend/mergeCapture.ml @@ -156,7 +156,7 @@ let process_merge_file deps_file = if Filename.is_relative target_results_dir then Filename.dirname (buck_out ()) // target_results_dir else target_results_dir in - let skiplevels = 2 in (** Don't link toplevel files, definitely not .start *) + let skiplevels = 2 in (* Don't link toplevel files, definitely not .start *) if should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst then slink ~stats ~skiplevels infer_out_src infer_out_dst | _ -> diff --git a/infer/src/backend/modelBuiltins.mli b/infer/src/backend/modelBuiltins.mli index 8bd152629..cbb36ea05 100644 --- a/infer/src/backend/modelBuiltins.mli +++ b/infer/src/backend/modelBuiltins.mli @@ -19,7 +19,9 @@ val __get_array_length : Procname.t val __get_type_of : Procname.t val __infer_fail : Procname.t val __instanceof : Procname.t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *) + val __cast : Procname.t (** [__cast(val,typ)] implements java's [typ(val)] *) + val __placement_delete : Procname.t val __placement_new : Procname.t val __new : Procname.t diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 1d41f8158..0f9d88ab8 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -122,7 +122,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let callee_pname = Cfg.Procdesc.get_proc_name callee_pdesc in - (** Dot means start of a procedure *) + (* Dot means start of a procedure *) L.log_progress_procedure (); if trace () then L.stderr "[%d] run_proc_analysis %a -> %a@." !nesting diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index ba03fb5ab..b8e8f760a 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -167,22 +167,23 @@ end = struct if include_subtrace then Pcall(p, pname, p_sub, get_dummy_stats ()) else p - module Invariant = (** functions in this module either do not assume, or do not re-establish, the invariant on dummy stats *) - struct + (** functions in this module either do not assume, or do not re-establish, the invariant on dummy + stats *) + module Invariant = struct (** check whether a stats is the dummy stats *) let stats_is_dummy stats = stats.max_length == - 1 - (** return the stats of the path *) - (** assumes that the stats are computed *) + (** return the stats of the path, assumes that the stats are computed *) let get_stats = function | Pstart (_, stats) -> stats | Pnode (_, _, _, _, stats, _) -> stats | Pjoin (_, _, stats) -> stats | Pcall (_, _, _, stats) -> stats - (** restore the invariant that all the stats are dummy, so the path is ready for another traversal *) - (** assumes that the stats are computed beforehand, and ensures that the invariant holds afterwards *) + (** restore the invariant that all the stats are dummy, so the path is ready for another + traversal assumes that the stats are computed beforehand, and ensures that the invariant + holds afterwards *) let rec reset_stats = function | Pstart (_, stats) -> if not (stats_is_dummy stats) then set_dummy_stats stats @@ -207,12 +208,13 @@ end = struct set_dummy_stats stats end - (** Iterate [f] over the path and compute the stats, assuming the invariant: all the stats are dummy. *) - (** Function [f] (typically with side-effects) is applied once to every node, and max_length in the stats - is the length of a longest sequence of nodes in the path where [f] returned [true] on at least one node. - max_length is 0 if the path was visited but no node satisfying [f] was found. *) - (** Assumes that the invariant holds beforehand, and ensures that all the stats are computed afterwards. *) - (** Since this breaks the invariant, it must be followed by reset_stats. *) + (** Iterate [f] over the path and compute the stats, assuming the invariant: all the stats are + dummy. Function [f] (typically with side-effects) is applied once to every node, and + max_length in the stats is the length of a longest sequence of nodes in the path where [f] + returned [true] on at least one node. max_length is 0 if the path was visited but no node + satisfying [f] was found. Assumes that the invariant holds beforehand, and ensures that all + the stats are computed afterwards. Since this breaks the invariant, it must be followed by + reset_stats. *) let rec compute_stats do_calls (f : Cfg.Node.t -> bool) = let nodes_found stats = stats.max_length > 0 in function diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 68c2c9b46..b515c1ae7 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -246,9 +246,9 @@ module CopyProp = let do_copy_propagation pdesc tenv = let proc_cfg = ExceptionalOneInstrPerNodeCfg.from_pdesc pdesc in let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) in - (** [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some - ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an - ident. *) + (* [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some + ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an + ident. *) let id_sub var_map id = (* [last_id] is the highest identifier in the chain that we've seen so far *) let rec id_sub_inner var_map var last_id = @@ -262,7 +262,7 @@ let do_copy_propagation pdesc tenv = Sil.Var last_id in id_sub_inner var_map (Var.of_id id) id in - (** perform copy-propagation on each instruction in [node] *) + (* perform copy-propagation on each instruction in [node] *) let rev_transform_node_instrs node = IList.fold_left (fun (instrs, changed) (instr, id_opt) -> diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 26bdaa034..dffe62466 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -27,6 +27,7 @@ let unSome = function | _ -> assert false type normal (** kind for normal props, i.e. normalized *) + type exposed (** kind for exposed props *) type pi = Sil.atom list @@ -322,7 +323,7 @@ let pp_prop pe0 f prop = end else F.fprintf f "%a%a%a" pp_pure () (pp_sigma pe) prop.sigma (pp_footprint pe) prop in - if !Config.forcing_delayed_prints then (** print in html mode *) + if !Config.forcing_delayed_prints then (* print in html mode *) F.fprintf f "%a%a%a" Io_infer.Html.pp_start_color Blue do_print () Io_infer.Html.pp_end_color () else do_print f () (** print in text mode *) @@ -927,9 +928,8 @@ let mk_inequality e = (** Normalize an inequality *) let inequality_normalize a = - (** turn an expression into a triple (pos,neg,off) of positive and negative occurrences, - and integer offset *) - (** representing inequality [sum(pos) - sum(neg) + off <= 0] *) + (* turn an expression into a triple (pos,neg,off) of positive and negative occurrences, and + integer offset representing inequality [sum(pos) - sum(neg) + off <= 0] *) let rec exp_to_posnegoff e = match e with | Sil.Const (Const.Cint n) -> [],[], n | Sil.BinOp(Binop.PlusA, e1, e2) | Sil.BinOp(Binop.PlusPI, e1, e2) -> @@ -946,7 +946,7 @@ let inequality_normalize a = let pos1, neg1, n1 = exp_to_posnegoff e1 in (neg1, pos1, IntLit.zero -- n1) | _ -> [e],[], IntLit.zero in - (** sort and filter out expressions appearing in both the positive and negative part *) + (* sort and filter out expressions appearing in both the positive and negative part *) let normalize_posnegoff (pos, neg, off) = let pos' = IList.sort Sil.exp_compare pos in let neg' = IList.sort Sil.exp_compare neg in @@ -959,7 +959,7 @@ let inequality_normalize a = | ps, ng -> (IList.rev pacc) @ ps, (IList.rev nacc) @ ng in let pos'', neg'' = combine [] [] (pos', neg') in (pos'', neg'', off) in - (** turn a non-empty list of expressions into a sum expression *) + (* turn a non-empty list of expressions into a sum expression *) let rec exp_list_to_sum = function | [] -> assert false | [e] -> e @@ -1423,6 +1423,7 @@ let pi_normalize_prop prop pi = Config.run_with_abs_val_equal_zero (pi_normalize prop.sub prop.sigma) pi (** {2 Compaction} *) + (** Return a compact representation of the prop *) let prop_compact sh prop = let sigma' = IList.map (Sil.hpred_compact sh) prop.sigma in @@ -2502,7 +2503,7 @@ type 'a prop_iter = { pit_sub : Sil.subst; (** substitution for equalities *) pit_pi : pi; (** pure part *) pit_newpi : (bool * Sil.atom) list; (** newly added atoms. *) - (** The first records !Config.footprint. *) + (* The first records !Config.footprint. *) pit_old : sigma; (** sigma already visited *) pit_curr : Sil.hpred; (** current element *) pit_state : 'a; (** state of current element *) diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 1358a58c4..cea5d5340 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -15,6 +15,7 @@ open! Utils open Sil type normal (** kind for normal props, i.e. normalized *) + type exposed (** kind for exposed props *) (** Proposition. *) @@ -204,6 +205,7 @@ val normalize : exposed t -> normal t val expose : normal t -> exposed t (** {2 Compaction} *) + (** Return a compact representation of the prop *) val prop_compact : sharing_env -> normal t -> normal t diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 6e9e70f18..2c0f09ce8 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -913,7 +913,8 @@ module ProverState : sig val reset : Prop.normal Prop.t -> Prop.exposed Prop.t -> unit val checks : check list ref - type bounds_check = (** type for array bounds checks *) + (** type for array bounds checks *) + type bounds_check = | BClen_imply of Sil.exp * Sil.exp * Sil.exp list (** coming from array_len_imply *) | BCfrom_pre of Sil.atom (** coming implicitly from preconditions *) @@ -1800,7 +1801,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 with | IMPL_EXC (s, _, _) when calc_missing -> raise (MISSING_EXC s)) - | Sil.Hlseg (Sil.Lseg_NE, para1, e1, f1, elist1), _ -> (** Unroll lseg *) + | Sil.Hlseg (Sil.Lseg_NE, para1, e1, f1, elist1), _ -> (* Unroll lseg *) let n' = Sil.Var (Ident.create_fresh Ident.kprimed) in let (_, para_inst1) = Sil.hpara_instantiate para1 e1 n' elist1 in let hpred_list1 = para_inst1@[Prop.mk_lseg Sil.Lseg_PE para1 n' f1 elist1] in @@ -1812,7 +1813,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 L.d_decrease_indent 1; res | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ - when Sil.exp_equal (Sil.exp_sub (fst subs) iF1) e2 -> (** Unroll dllseg forward *) + when Sil.exp_equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *) let n' = Sil.Var (Ident.create_fresh Ident.kprimed) in let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iF1 oB1 n' elist1 in let hpred_list1 = para_inst1@[Prop.mk_dllseg Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1] in @@ -1824,7 +1825,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 L.d_decrease_indent 1; res | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ - when Sil.exp_equal (Sil.exp_sub (fst subs) iB1) e2 -> (** Unroll dllseg backward *) + when Sil.exp_equal (Sil.exp_sub (fst subs) iB1) e2 -> + (* Unroll dllseg backward *) let n' = Sil.Var (Ident.create_fresh Ident.kprimed) in let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iB1 n' oF1 elist1 in let hpred_list1 = para_inst1@[Prop.mk_dllseg Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1] in @@ -1924,7 +1926,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 let _, para_inst2 = if Sil.exp_equal iF2 iB2 then Sil.hpara_dll_instantiate para2 iF2 oB2 oF2 elist2 - else assert false in (** Only base case of rhs list considered for now *) + else assert false in (* Only base case of rhs list considered for now *) L.d_increase_indent 1; let res = decrease_indent_when_exception @@ -1932,7 +1934,7 @@ 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' -> (** Only consider implications between identical listsegs for now *) + | Some iter1' -> (* Only consider implications between identical listsegs for now *) let elist2 = IList.map (fun e -> Sil.exp_sub (snd subs) e) elist2 in let subs' = exp_list_imply calc_missing subs (iF2:: oB2:: oF2:: iB2:: elist2) (iF2:: oB2:: oF2:: iB2:: elist2) in (* force instantiation of existentials *) let prop1' = Prop.prop_iter_remove_curr_then_to_prop iter1' diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index beb13d615..6e0966c67 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -634,7 +634,7 @@ let add_guarded_by_constraints prop lexp pdesc = (* programmers write @GuardedBy("MyClass.class") when the field is guarded by the class *) guarded_by_str_is_class guarded_by_str (Procname.java_get_class_name java_pname) | _ -> false in - (** return true if [guarded_by_str] is as suffix of ".this" *) + (* return true if [guarded_by_str] is as suffix of ".this" *) let guarded_by_str_is_current_class_this guarded_by_str = function | Procname.Java java_pname -> let fully_qualified_this = @@ -653,7 +653,7 @@ let add_guarded_by_constraints prop lexp pdesc = else None in IList.find_map_opt annot_extract_guarded_by_str item_annot in - (** if [fld] is annotated with @GuardedBy("mLock"), return mLock *) + (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *) let get_guarded_by_fld_str fld typ = match Annotations.get_field_type_and_annotation fld typ with | Some (_, item_annot) -> diff --git a/infer/src/backend/rearrange.mli b/infer/src/backend/rearrange.mli index 073cf0be2..d8cbbad96 100644 --- a/infer/src/backend/rearrange.mli +++ b/infer/src/backend/rearrange.mli @@ -18,9 +18,8 @@ exception ARRAY_ACCESS val check_dereference_error : Cfg.Procdesc.t -> Prop.normal Prop.t -> Sil.exp -> Location.t -> unit -(** Check that an expression representing an objc block - can be null and raise a [B1] null exception. *) -(** It's used to check that we don't call possibly null blocks *) +(** Check that an expression representing an objc block can be null and raise a [B1] null exception. + It's used to check that we don't call possibly null blocks *) val check_call_to_objc_block_error : Cfg.Procdesc.t -> Prop.normal Prop.t -> Sil.exp -> Location.t -> unit diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 43ec83745..4aec941c4 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -168,11 +168,16 @@ let visited_str vis = visited: a list of pairs (node_id, line) for the visited nodes *) type 'a spec = { pre: 'a Jprop.t; posts: ('a Prop.t * Paths.Path.t) list; visited : Visitedset.t } -module NormSpec : sig (* encapsulate type for normalized specs *) +(** encapsulate type for normalized specs *) +module NormSpec : sig type t + val normalize : Prop.normal spec -> t + val tospecs : t list -> Prop.normal spec list + val compact : Sil.sharing_env -> t -> t (** Return a compact representation of the spec *) + val erase_join_info_pre : t -> t (** Erase join info from pre of spec *) end = struct type t = Prop.normal spec @@ -226,7 +231,8 @@ module CallStats = struct (** module for tracing stats of function calls *) Location.equal loc1 loc2 && Procname.equal pname1 pname2 end) - type call_result = (** kind of result of a procedure call *) + (** kind of result of a procedure call *) + type call_result = | CR_success (** successful call *) | CR_not_met (** precondition not met *) | CR_not_found (** the callee has no specs *) diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index a577b8403..9129d1917 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -72,15 +72,17 @@ val visited_str : Visitedset.t -> string visited: a list of pairs (node_id, line) for the visited nodes *) type 'a spec = { pre: 'a Jprop.t; posts: ('a Prop.t * Paths.Path.t) list; visited : Visitedset.t } -module NormSpec : sig (* encapsulate type for normalized specs *) +(** encapsulate type for normalized specs *) +module NormSpec : sig type t end -module CallStats : (** module for tracing stats of function calls *) -sig +(** module for tracing stats of function calls *) +module CallStats : sig type t - type call_result = (** kind of result of a procedure call *) + (** kind of result of a procedure call *) + type call_result = | CR_success (** successful call *) | CR_not_met (** precondition not met *) | CR_not_found (** the callee has no specs *) @@ -206,13 +208,13 @@ val is_inactive : Procname.t -> bool (** Initialize the summary for [proc_name] given dependent procs in list [depend_list]. Do nothing if a summary exists already. *) val init_summary : - (Procname.t list * (** depend list *) - Cfg.Node.id list * (** nodes *) - proc_flags * (** procedure flags *) - (Procname.t * Location.t) list * (** calls *) - (Cg.in_out_calls option) * (** in and out calls *) - ProcAttributes.t) (** attributes of the procedure *) - -> unit + (Procname.t list * (* depend list *) + Cfg.Node.id list * (* nodes *) + proc_flags * (* procedure flags *) + (Procname.t * Location.t) list * (* calls *) + (Cg.in_out_calls option) * (* in and out calls *) + ProcAttributes.t (* attributes of the procedure *) + ) -> unit (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) val reset_summary : Cg.t -> Procname.t -> ProcAttributes.t option -> unit diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index db9e2a489..b553eef8f 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -31,32 +31,32 @@ type failure_stats = { module NodeHash = Cfg.NodeHash type t = { - (** Constant map for the procedure *) mutable const_map : const_map; + (** Constant map for the procedure *) - (** Diverging states since the last reset for the node *) mutable diverging_states_node : Paths.PathSet.t; + (** Diverging states since the last reset for the node *) - (** Diverging states since the last reset for the procedure *) mutable diverging_states_proc : Paths.PathSet.t; + (** Diverging states since the last reset for the procedure *) - (** Last instruction seen *) mutable last_instr : Sil.instr option; + (** Last instruction seen *) - (** Last node seen *) mutable last_node : Cfg.Node.t; + (** Last node seen *) - (** Last path seen *) mutable last_path : (Paths.Path.t * (Sil.path_pos option)) option; + (** Last path seen *) - (** Last prop,tenv,pdesc seen *) mutable last_prop_tenv_pdesc : (Prop.normal Prop.t * Tenv.t * Cfg.Procdesc.t) option; + (** Last prop,tenv,pdesc seen *) - (** Last session seen *) mutable last_session : int; + (** Last session seen *) - (** Map visited nodes to failure statistics *) failure_map : failure_stats NodeHash.t; + (** Map visited nodes to failure statistics *) } let initial () = { diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index c0febe0a2..0dc9634a6 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1134,7 +1134,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames | Sil.Call (ret_ids, Sil.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> - (** Generic fun call with known name *) + (* Generic fun call with known name *) let (prop_r, n_actual_params) = normalize_params current_pname prop_ actual_params in let resolved_pname = match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with @@ -1195,7 +1195,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path proc_call (Option.get summary) (call_args prop resolved_pname n_actual_params ret_ids loc) in IList.flatten (IList.map do_call sentinel_result) - | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *) + | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (* Call via function pointer *) let (prop_r, n_actual_params) = normalize_params current_pname prop_ actual_params in if call_flags.CallFlags.cf_is_objc_block then Rearrange.check_call_to_objc_block_error current_pdesc prop_r fun_exp loc; @@ -1618,7 +1618,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= act and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), path) : Paths.PathSet.t = let pname = Cfg.Procdesc.get_proc_name pdesc in - let prop_primed_to_normal p = (** Rename primed vars with fresh normal vars, and return them *) + let prop_primed_to_normal p = (* Rename primed vars with fresh normal vars, and return them *) let fav = Prop.prop_fav p in Sil.fav_filter_ident fav Ident.is_primed; let ids_primed = Sil.fav_to_list fav in @@ -1706,7 +1706,7 @@ let node handle_exn tenv node (pset : Paths.PathSet.t) : Paths.PathSet.t = end else sym_exec_wrapper handle_exn tenv pdesc instr (p, tr) in Paths.PathSet.union pset2 pset1 in - let exe_instr_pset (pset, stack) instr = (** handle a single instruction at the set level *) + let exe_instr_pset (pset, stack) instr = (* handle a single instruction at the set level *) let pp_stack_instr pset' = L.d_str "Stack Instruction "; Sil.d_instr instr; L.d_ln (); L.d_strln "Stack Instruction Returns"; diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index da060f2db..dfe5cdc6a 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -30,25 +30,25 @@ type deref_error = | Deref_freed of Sil.res_action (** dereference a freed pointer *) | Deref_minusone (** dereference -1 *) | Deref_null of Sil.path_pos (** dereference null *) - (** dereference a value coming from the given undefined function *) | Deref_undef of Procname.t * Location.t * Sil.path_pos + (** dereference a value coming from the given undefined function *) | Deref_undef_exp (** dereference an undefined expression *) type invalid_res = - (** dereference error and description *) | Dereference_error of deref_error * Localise.error_desc * Paths.Path.t option + (** dereference error and description *) - (** the abduction prover failed some checks *) | Prover_checks of Prover.check list + (** the abduction prover failed some checks *) - (** cannot combine actual pre with splitting and post *) | Cannot_combine + (** cannot combine actual pre with splitting and post *) - (** missing_fld not empty in re-execution mode *) | Missing_fld_not_empty + (** missing_fld not empty in re-execution mode *) - (** missing sigma not empty in re-execution mode *) | Missing_sigma_not_empty + (** missing sigma not empty in re-execution mode *) type valid_res = { incons_pre_missing : bool; (** whether the actual pre is consistent with the missing part *) @@ -184,7 +184,7 @@ let process_splitting match Sil.exp_sub sub1_inverse (Sil.Var id) with | Sil.Var id' -> if Sil.fav_mem fav_actual_pre id' || Ident.is_path id' - (** a path id represents a position in the pre *) + (* a path id represents a position in the pre *) then Sil.Var id' else Sil.Var (Ident.create_fresh Ident.kprimed) | _ -> assert false in @@ -355,7 +355,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = let post_process_sigma (sigma: Sil.hpred list) loc : Sil.hpred list = let map_inst inst = Sil.inst_new_loc loc inst in let do_hpred (_, _, hpred) = Sil.hpred_instmap map_inst hpred in - (** update the location of instrumentations *) + (* update the location of instrumentations *) IList.map (fun hpred -> do_hpred (Prover.expand_hpred_pointer false hpred)) sigma (** check for interprocedural path errors in the post *) @@ -603,7 +603,7 @@ let prop_copy_footprint_pure p1 p2 = let pi2_attr, pi2_noattr = IList.partition Prop.atom_is_attribute pi2 in let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *) - (** if [atom] represents an attribute [att], add the attribure to [prop] *) + (* if [atom] represents an attribute [att], add the attribure to [prop] *) match Prop.atom_get_exp_attribute atom with | None -> prop | Some (exp, att) -> @@ -738,7 +738,7 @@ let combine let post_p1' = Prop.replace_sigma post_p1_sigma' post_p1 in Prop.normalize (Prop.replace_pi (Prop.get_pi post_p1 @ split.missing_pi) post_p1') in - let post_p3 = (** replace [result|callee] with an aux variable dedicated to this proc *) + let post_p3 = (* replace [result|callee] with an aux variable dedicated to this proc *) let callee_ret_pvar = Sil.Lvar (Pvar.to_callee callee_pname (Pvar.get_ret_pvar callee_pname)) in match Prop.prop_iter_create post_p2 with @@ -768,7 +768,7 @@ let combine | _ -> p in let p = Prop.prop_iter_remove_curr_then_to_prop iter' in do_ftl_ids p (ftl, ret_ids) - | Sil.Hpointsto _ -> (** returning nothing or unexpected sexp, turning into nondet *) + | Sil.Hpointsto _ -> (* returning nothing or unexpected sexp, turning into nondet *) Prop.prop_iter_remove_curr_then_to_prop iter' | _ -> assert false in let post_p4 = @@ -1118,7 +1118,7 @@ let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = let new_footprint_atoms = IList.filter is_footprint_atom_not_attribute pure in if new_footprint_atoms == [] then p - else (** add pure fact to footprint *) + else (* add pure fact to footprint *) Prop.normalize (Prop.replace_pi_footprint (Prop.get_pi_footprint p @ new_footprint_atoms) p) (** post-process the raw result of a function call *) diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index f0e7504d7..573dc11d3 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -17,11 +17,11 @@ module F = Format (** status of a timeout instance *) type status = { - (** Seconds remaining in the current timeout *) seconds_remaining : float; + (** Seconds remaining in the current timeout *) - (** Internal State of SymOp *) symop_state : SymOp.t + (** Internal State of SymOp *) } (** stack of suspended timeout instances *) diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index ad07c2550..63560b711 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -347,8 +347,8 @@ let copy_file fname_from fname_to = cleanup(); None -module FileLOC = (** count lines of code of files and keep processed results in a cache *) -struct +(** count lines of code of files and keep processed results in a cache *) +module FileLOC = struct let include_loc_hash = Hashtbl.create 1 let reset () = Hashtbl.clear include_loc_hash diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 9a99056ba..fc5d126fb 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -205,9 +205,10 @@ val filename_to_absolute : string -> string (** Convert an absolute filename to one relative to a root directory *) val filename_to_relative : string -> string -> string -module FileLOC : (** count lines of code of files and keep processed results in a cache *) -sig +(** count lines of code of files and keep processed results in a cache *) +module FileLOC : sig val reset: unit -> unit (** reset the cache *) + val file_get_loc : string -> int (** get the LOC of the file *) end @@ -230,7 +231,9 @@ val close_outf : outfile -> unit type proc_flags = (string, string) Hashtbl.t (** keys for proc_flags *) + val proc_flag_skip : string (** key to specify that a function should be treated as a skip function *) + val proc_flag_ignore_return : string (** key to specify that it is OK to ignore the return value *) (** empty proc flags *) diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml index ed107bee9..7f8dd9995 100644 --- a/infer/src/checkers/BoundedCallTree.ml +++ b/infer/src/checkers/BoundedCallTree.ml @@ -65,7 +65,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct string_equal frame.Stacktrace.class_str (Procname.objc_cpp_get_class_name objc_cpp_prod) - | Procname.C _ -> true (** Needed for test code. *) + | Procname.C _ -> true (* Needed for test code. *) | Procname.Block _ -> failwith "Proc type not supported by crashcontext: block" in frame.Stacktrace.method_str = (Procname.get_method caller) && @@ -86,9 +86,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else astate | Sil.Call _ -> - (** We currently ignore calls through function pointers in C and - * other potential special kinds of procedure calls to be added later, - * e.g. Java reflection. *) + (* We currently ignore calls through function pointers in C and + other potential special kinds of procedure calls to be added later, + e.g. Java reflection. *) astate | Sil.Letderef _ | Set _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _ | Abstract _ | Nullify _ -> @@ -102,13 +102,12 @@ module Analyzer = (TransferFunctions) (** Stacktrace lookup: - * 1) Check if trace_ref is already set and use that. - * 2) If not, load trace from the file specified in Config.stacktrace. *) + 1) Check if trace_ref is already set and use that. + 2) If not, load trace from the file specified in Config.stacktrace. *) let trace_ref = ref None let load_trace () = - (** Check Config.stacktrace is set and points to a file, - * call Stacktrace.of_json_file *) + (* Check Config.stacktrace is set and points to a file, call Stacktrace.of_json_file *) let filename = match Config.stacktrace with | None -> failwith "Missing command line option: '--stacktrace stack.json' \ must be used when running '-a crashcontext'. This \ diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index 8e7cd0bda..1d3b2b33e 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -241,7 +241,7 @@ module BooleanVars = struct (** Transfer function for an instruction. *) let do_instr _ _ idenv (instr : Sil.instr) (state : State.t) : State.t = - (** Normalize a boolean condition. *) + (* Normalize a boolean condition. *) let normalize_condition cond_e = match cond_e with | Sil.UnOp (Unop.LNot, Sil.BinOp (Binop.Eq, e1, e2), _) -> @@ -250,7 +250,7 @@ module BooleanVars = struct Sil.BinOp (Binop.Eq, e1, e2) | _ -> cond_e in - (** Normalize an instruction. *) + (* Normalize an instruction. *) let normalize_instr = function | Sil.Prune (cond_e, loc, tb, ik) -> let cond_e' = normalize_condition cond_e in diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index acec4139d..e20da7a3d 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -410,7 +410,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p let ret_const_key = "return_const" in let reverse_find_instr f node = - (** this is not really sound but for the moment a sufficient approximation *) + (* this is not really sound but for the moment a sufficient approximation *) let has_instr node = try ignore(IList.find f (Cfg.Node.get_instrs node)); true with Not_found -> false in @@ -451,10 +451,10 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p | Sil.Set (e1, _, _, _) when Sil.exp_equal expanded e1 -> true | _ -> false in match reverse_find_instr is_set_instr node with - (** Look for ivar := tmp *) + (* Look for ivar := tmp *) | Some s -> ( match reverse_find_instr (is_call_instr s) node with - (** Look for tmp := foo() *) + (* Look for tmp := foo() *) | Some (Sil.Call (_, Sil.Const (Const.Cfun pn), _, _, _)) -> get_return_const pn | _ -> "?") diff --git a/infer/src/checkers/checkers.mli b/infer/src/checkers/checkers.mli index b360c30af..76a5cf4b9 100644 --- a/infer/src/checkers/checkers.mli +++ b/infer/src/checkers/checkers.mli @@ -16,6 +16,7 @@ open! Utils module ST : sig (** Add a key/value pair. *) val pname_add : Procname.t -> string -> string -> unit + (** Find the value associated to the key. Raise Not_found if it does not exist. *) val pname_find: Procname.t -> string -> string diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 58d5cc93f..5163a7de7 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -18,14 +18,20 @@ type throws = (** Module type used to define the state component for a dataflow algorithm. *) module type DFStateType = sig - type t (** Type for state. *) - val equal : t -> t -> bool (** Equality between states. *) - val join : t -> t -> t (** Join two states (the old one is the first parameter). *) + (** Type for state. *) + type t + + (** Equality between states. *) + val equal : t -> t -> bool + + (** Join two states (the old one is the first parameter). *) + val join : t -> t -> t (** Perform a state transition on a node. *) val do_node : Tenv.t -> Cfg.Node.t -> t -> (t list) * (t list) - val proc_throws : Procname.t -> throws (** Can proc throw an exception? *) + (** Can proc throw an exception? *) + val proc_throws : Procname.t -> throws end (** Type for the dataflow API. *) diff --git a/infer/src/checkers/dataflow.mli b/infer/src/checkers/dataflow.mli index 39612477f..836634c4f 100644 --- a/infer/src/checkers/dataflow.mli +++ b/infer/src/checkers/dataflow.mli @@ -16,14 +16,20 @@ type throws = (** Module type used to define the state component for a dataflow algorithm. *) module type DFStateType = sig - type t (** Type for state. *) - val equal : t -> t -> bool (** Equality between states. *) - val join : t -> t -> t (** Join two states (the old one is the first parameter). *) + (** Type for state. *) + type t + + (** Equality between states. *) + val equal : t -> t -> bool + + (** Join two states (the old one is the first parameter). *) + val join : t -> t -> t (** Perform a state transition on a node. *) val do_node : Tenv.t -> Cfg.Node.t -> t -> (t list) * (t list) - val proc_throws : Procname.t -> throws (** Can proc throw an exception? *) + (** Can proc throw an exception? *) + val proc_throws : Procname.t -> throws end (** Type for the dataflow API. *) @@ -34,6 +40,7 @@ module type DF = sig | Dead_state | Transition of state * state list * state list val join : state list -> state -> state + (** Run the dataflow analysis on a procedure starting from the given state. Returns a function to lookup the results of the analysis on every node *) val run : Tenv.t -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index fd127455e..e6d1b93bd 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -72,26 +72,38 @@ module type S = sig (** get the instructions from a node *) val instrs : node -> Sil.instr list + (** explode a block into its instructions and an optional id for the instruction. the purpose of this is to specify a policy for fine-grained storage of invariants by the abstract interpreter. the interpreter will forget invariants at program points where the id is None, and remember them otherwise *) val instr_ids : node -> (Sil.instr * id option) list + val succs : t -> node -> node list + (** all predecessors (normal and exceptional) *) val preds : t -> node -> node list + (** non-exceptional successors *) val normal_succs : t -> node -> node list + (** non-exceptional predecessors *) val normal_preds : t -> node -> node list + (** exceptional successors *) val exceptional_succs : t -> node -> node list + (** exceptional predescessors *) val exceptional_preds : t -> node -> node list + val start_node : t -> node + val exit_node : t -> node + val proc_desc : t -> Cfg.Procdesc.t + val nodes : t -> node list + val from_pdesc : Cfg.Procdesc.t -> t end diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index c1c955d47..333ca0a26 100644 --- a/infer/src/checkers/procCfg.mli +++ b/infer/src/checkers/procCfg.mli @@ -31,26 +31,38 @@ module type S = sig (** get the instructions from a node *) val instrs : node -> Sil.instr list + (** explode a block into its instructions and an optional id for the instruction. the purpose of this is to specify a policy for fine-grained storage of invariants by the abstract interpreter. the interpreter will forget invariants at program points where the id is None, and remember them otherwise *) val instr_ids : node -> (Sil.instr * id option) list + val succs : t -> node -> node list + (** all predecessors (normal and exceptional) *) val preds : t -> node -> node list + (** non-exceptional successors *) val normal_succs : t -> node -> node list + (** non-exceptional predecessors *) val normal_preds : t -> node -> node list + (** exceptional successors *) val exceptional_succs : t -> node -> node list + (** exceptional predescessors *) val exceptional_preds : t -> node -> node list + val start_node : t -> node + val exit_node : t -> node + val proc_desc : t -> Cfg.Procdesc.t + val nodes : t -> node list + val from_pdesc : Cfg.Procdesc.t -> t end diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index 4d684b110..692e0faa4 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -108,7 +108,7 @@ struct (** Check repeated calls to the same procedure. *) let check_instr tenv get_proc_desc curr_pname curr_pdesc extension instr normalized_etl = - (** Arguments are not temporary variables. *) + (* Arguments are not temporary variables. *) let arguments_not_temp args = let filter_arg (e, _) = match e with | Sil.Lvar pvar -> diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index fd26b888c..257f9b639 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -82,9 +82,11 @@ val ivar_to_property_index : Clang_ast_t.decl Clang_ast_main.PointerMap.t ref val json : string ref val pointer_decl_index : Clang_ast_t.decl Clang_ast_main.PointerMap.t ref val pointer_stmt_index : Clang_ast_t.stmt Clang_ast_main.PointerMap.t ref + (** Map from clang pointers to types produced by ast exporter. Populated once on InferClang startup *) val pointer_type_index : Clang_ast_t.c_type Clang_ast_main.PointerMap.t ref + (** Map from type pointers (clang pointers and types created later by frontend) to sil types Populated during frontend execution when new type is found *) val sil_types_map : (Typ.t Clang_ast_types.TypePointerMap.t) ref diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index cbcaafb57..b44c5244d 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -9,8 +9,8 @@ open! Utils -(** Methods for creating a procdesc from a method or function declaration *) -(** and for resolving a method call and finding the right callee *) +(** Methods for creating a procdesc from a method or function declaration + and for resolving a method call and finding the right callee *) open CFrontend_utils @@ -18,11 +18,10 @@ module L = Logging exception Invalid_declaration -(** When the methoc call is MCStatic, means that it is a class method. *) -(** When it is MCVirtual, it means that it is an instance method and that *) -(** the method to be called will be determined at runtime. If it is MCNoVirtual *) -(** it means that it is an instance method but that the method to be called will *) -(** be determined at compile time *) +(** When the methoc call is MCStatic, means that it is a class method. When it is MCVirtual, it + means that it is an instance method and that the method to be called will be determined at + runtime. If it is MCNoVirtual it means that it is an instance method but that the method to be + called will be determined at compile time *) type method_call_type = | MCVirtual | MCNoVirtual diff --git a/infer/src/clang/cMethod_trans.mli b/infer/src/clang/cMethod_trans.mli index f1ac02bed..2679084d4 100644 --- a/infer/src/clang/cMethod_trans.mli +++ b/infer/src/clang/cMethod_trans.mli @@ -12,11 +12,10 @@ open! Utils (** Methods for creating a procdesc from a method or function declaration and for resolving a method call and finding the right callee *) -(** When the methoc call is MCStatic, means that it is a class method. *) -(** When it is MCVirtual, it means that it is an instance method and that *) -(** the method to be called will be determined at runtime. If it is MCNoVirtual *) -(** it means that it is an instance method but that the method to be called will *) -(** be determined at compile time *) +(** When the methoc call is MCStatic, means that it is a class method. When it is MCVirtual, it + means that it is an instance method and that the method to be called will be determined at + runtime. If it is MCNoVirtual it means that it is an instance method but that the method to be + called will be determined at compile time *) type method_call_type = | MCVirtual | MCNoVirtual diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 6a39f0b95..e0b98c274 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -20,9 +20,9 @@ module L = Logging module type CTrans = sig (** Translates instructions: (statements and expressions) from the ast into sil *) - (** It receives the context, a list of statements from clang ast, list of custom statments *) - (** to be added before clang statements and the exit node and it returns a list of cfg nodes *) - (** that reporesent the translation of the stmts into sil. *) + (** It receives the context, a list of statements from clang ast, list of custom statments to be + added before clang statements and the exit node and it returns a list of cfg nodes that + reporesent the translation of the stmts into sil. *) val instructions_trans : CContext.t -> Clang_ast_t.stmt -> CModule_type.instr_type list -> Cfg.Node.t -> Cfg.Node.t list diff --git a/infer/src/clang/cTrans.mli b/infer/src/clang/cTrans.mli index e4906a282..c9639e3f8 100644 --- a/infer/src/clang/cTrans.mli +++ b/infer/src/clang/cTrans.mli @@ -10,11 +10,10 @@ open! Utils module type CTrans = sig - (** Translates instructions: (statements and expressions) from the ast into sil *) - - (** It receives the context, a list of statements from clang ast, list of custom statments *) - (** to be added before clang statements and the exit node and it returns a list of cfg nodes *) - (** that reporesent the translation of the stmts into sil. *) + (** Translates instructions: (statements and expressions) from the ast into sil. It receives the + context, a list of statements from clang ast, list of custom statments to be added before + clang statements and the exit node and it returns a list of cfg nodes that reporesent the + translation of the stmts into sil. *) val instructions_trans : CContext.t -> Clang_ast_t.stmt -> CModule_type.instr_type list -> Cfg.Node.t -> Cfg.Node.t list diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index a89f84f3e..5177b5992 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -392,8 +392,8 @@ let dereference_var_sil (exp, typ) sil_loc = let sil_instr = Sil.Letderef (id, exp, typ, sil_loc) in ([sil_instr], Sil.Var id) -(** Given trans_result with ONE expression, create temporary variable with *) -(** value of an expression assigned to it *) +(** Given trans_result with ONE expression, create temporary variable with value of an expression + assigned to it *) let dereference_value_from_result sil_loc trans_result ~strip_pointer = let (obj_sil, class_typ) = extract_exp_from_list trans_result.exps "" in let cast_inst, cast_exp = dereference_var_sil (obj_sil, class_typ) sil_loc in diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 68a1d6b51..ae132f446 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -78,8 +78,8 @@ val is_member_exp : Clang_ast_t.stmt -> bool val get_type_from_exp_stmt : Clang_ast_t.stmt -> Clang_ast_t.type_ptr -(** Given trans_result with ONE expression, create temporary variable with *) -(** dereferenced value of an expression assigned to it *) +(** Given trans_result with ONE expression, create temporary variable with dereferenced value of an + expression assigned to it *) val dereference_value_from_result : Location.t -> trans_result -> strip_pointer:bool -> trans_result val cast_operation : @@ -142,18 +142,15 @@ sig end -(** 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 *) -(** 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 *) -(** priority first (like taking a lock). priority can be claimes only when *) -(** it is free. If an element of AST succedes in claiming priority its id *) -(** (pointer) is recorded in priority. After an element has finished it *) -(** frees the priority. In general an AST element E checks if an ancestor *) -(** has claimed priority. If priority is already claimed E does not have to *) -(** create a node. If priority is free then it means E has to create the *) -(** node. Then E claims priority and release it afterward. *) +(** 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 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 priority first + (like taking a lock). priority can be claimes only when it is free. If an element of AST + succedes in claiming priority its id (pointer) is recorded in priority. After an element has + finished it frees the priority. In general an AST element E checks if an ancestor has claimed + priority. If priority is already claimed E does not have to create a node. If priority is free + then it means E has to create the node. Then E claims priority and release it afterward. *) module PriorityNode : sig @@ -200,8 +197,8 @@ sig end -(** This module handles the translation of the variable self which is challenging because self *) -(** is used both as a variable in instance method calls and also as a type in class method calls. *) +(** This module handles the translation of the variable self which is challenging because self is + used both as a variable in instance method calls and also as a type in class method calls. *) module Self : sig diff --git a/infer/src/clang/objcInterface_decl.mli b/infer/src/clang/objcInterface_decl.mli index 96b08c241..11bb3cbe3 100644 --- a/infer/src/clang/objcInterface_decl.mli +++ b/infer/src/clang/objcInterface_decl.mli @@ -9,9 +9,8 @@ open! Utils -(** In this module an ObjC interface declaration is processed. The class *) -(** is saved in the tenv as a struct with the corresponding fields, potential superclass and *) -(** list of defined methods *) +(** In this module an ObjC interface declaration is processed. The class is saved in the tenv as a + struct with the corresponding fields, potential superclass and list of defined methods *) open CFrontend_utils val interface_declaration : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl -> diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 6304e8d68..ff1166797 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -86,7 +86,7 @@ struct let typestate_empty = TypeState.empty Extension.ext in IList.fold_left add_formal typestate_empty annotated_signature.Annotations.params in - (** Check the nullable flag computed for the return value and report inconsistencies. *) + (* Check the nullable flag computed for the return value and report inconsistencies. *) let check_return find_canonical_duplicate exit_node final_typestate ret_ia ret_type loc : unit = let ret_pvar = Cfg.Procdesc.get_ret_var curr_pdesc in let ret_range = TypeState.lookup_pvar ret_pvar final_typestate in @@ -190,7 +190,7 @@ struct type init = Procname.t * Cfg.Procdesc.t let final_typestates initializers_current_class = - (** Get the private methods, from the same class, directly called by the initializers. *) + (* Get the private methods, from the same class, directly called by the initializers. *) let get_private_called (initializers : init list) : init list = let res = ref [] in let do_proc (init_pn, init_pd) = @@ -216,8 +216,8 @@ struct IList.iter do_proc initializers; !res in - (** Get the initializers recursively called by computing a fixpoint. - Start from the initializers of the current class and the current procedure. *) + (* Get the initializers recursively called by computing a fixpoint. + Start from the initializers of the current class and the current procedure. *) let initializers_recursive : init list = let initializers_base_case = initializers_current_class in @@ -238,7 +238,7 @@ struct fixpoint initializers_base_case; !res in - (** Get the final typestates of all the initializers. *) + (* Get the final typestates of all the initializers. *) let final_typestates = ref [] in let get_final_typestate (pname, pdesc) = match typecheck_proc false pname pdesc None with diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index ebd32c13f..d93504f52 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -247,9 +247,9 @@ let typecheck_instr (* (TypeState.pp ext) typestate; *) (* L.stdout " %a@." (Sil.pp_instr pe_text) instr in *) - (** Handle the case where a field access X.f happens via a temporary variable $Txxx. - This has been observed in assignments this.f = exp when exp contains an ifthenelse. - Reconstuct the original expression knowing: the origin of $Txxx is 'this'. *) + (* Handle the case where a field access X.f happens via a temporary variable $Txxx. + This has been observed in assignments this.f = exp when exp contains an ifthenelse. + Reconstuct the original expression knowing: the origin of $Txxx is 'this'. *) let handle_field_access_via_temporary typestate exp = let name_is_temporary name = let prefix = "$T" in @@ -278,8 +278,8 @@ let typecheck_instr exp' | _ -> exp in - (** Convert a complex expressions into a pvar. - When [is_assigment] is true, update the relevant annotations for the pvar. *) + (* 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 default = exp, typestate in @@ -364,13 +364,13 @@ let typecheck_instr let typestate' = update_typestate_fld pvar fn typ in (Sil.Lvar pvar, typestate') | Sil.Lfield (_exp', fn', _) when Ident.java_fieldname_is_outer_instance fn' -> - (** handle double dereference when accessing a field from an outer class *) + (* handle double dereference when accessing a field from an outer class *) let fld_name = Ident.fieldname_to_string fn' ^ "_" ^ Ident.fieldname_to_string fn in let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let typestate' = update_typestate_fld pvar fn typ in (Sil.Lvar pvar, typestate') | Sil.Lvar _ | Sil.Lfield _ when ComplexExpressions.all_nested_fields () -> - (** treat var.field1. ... .fieldn as a constant *) + (* treat var.field1. ... .fieldn as a constant *) begin match ComplexExpressions.exp_to_string node' exp with | Some exp_str -> @@ -638,7 +638,7 @@ let typecheck_instr typestate' | _ :: _ :: _ -> assert false in - (** Handle Preconditions.checkNotNull. *) + (* Handle Preconditions.checkNotNull. *) let do_preconditions_check_not_null parameter_num is_vararg typestate' = (* clear the nullable flag of the first parameter of the procedure *) let clear_nullable_flag typestate'' pvar = @@ -686,7 +686,7 @@ let typecheck_instr | None -> typestate' in - (** Handle Preconditions.checkState for &&-separated conditions x!=null. *) + (* Handle Preconditions.checkState for &&-separated conditions x!=null. *) let do_preconditions_check_state typestate' = let handle_pvar ann b typestate1 pvar = (* handle the annotation flag for pvar *) match TypeState.lookup_pvar pvar typestate1 with @@ -751,7 +751,7 @@ let typecheck_instr end | _ -> typestate' in - (** Handle m.put(k,v) as assignment pvar = v for the pvar associated to m.get(k) *) + (* Handle m.put(k,v) as assignment pvar = v for the pvar associated to m.get(k) *) let do_map_put typestate' = (* Get the proc name for map.get() from map.put() *) let pname_get_from_pname_put pname_put = @@ -1029,8 +1029,8 @@ let typecheck_instr check_condition node' (Sil.BinOp (Binop.Eq, e1, e2)) | _ -> typestate in - (** Handle assigment fron a temp pvar in a condition. - This recognizes the handling of temp variables in ((x = ...) != null) *) + (* Handle assigment fron a temp pvar in a condition. + This recognizes the handling of temp variables in ((x = ...) != null) *) let handle_assignment_in_condition pvar = match Cfg.Node.get_preds node with | [prev_node] -> @@ -1044,7 +1044,7 @@ let typecheck_instr !found | _ -> None in - (** Normalize the condition by resolving temp variables. *) + (* Normalize the condition by resolving temp variables. *) let rec normalize_cond _node _cond = match _cond with | Sil.UnOp (Unop.LNot, c, top) -> let node', c' = normalize_cond _node c in diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index 71cb69f68..3965d98e4 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -24,9 +24,10 @@ type get_proc_desc = Procname.t -> Cfg.Procdesc.t option type 'a ext = { empty : 'a; (** empty extension *) - check_instr : (** check the extension for an instruction *) + check_instr : Tenv.t -> get_proc_desc -> Procname.t -> - Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a; + Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> + 'a; (** check the extension for an instruction *) join : 'a -> 'a -> 'a; (** join two extensions *) pp : Format.formatter -> 'a -> unit (** pretty print an extension *) } diff --git a/infer/src/eradicate/typeState.mli b/infer/src/eradicate/typeState.mli index 7c24ab632..32c2fe7d8 100644 --- a/infer/src/eradicate/typeState.mli +++ b/infer/src/eradicate/typeState.mli @@ -20,9 +20,10 @@ type get_proc_desc = Procname.t -> Cfg.Procdesc.t option type 'a ext = { empty : 'a; (** empty extension *) - check_instr : (** check the extension for an instruction *) + check_instr : Tenv.t -> get_proc_desc -> Procname.t -> - Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> 'a; + Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> + 'a; (** check the extension for an instruction *) join : 'a -> 'a -> 'a; (** join two extensions *) pp : Format.formatter -> 'a -> unit (** pretty print an extension *) } diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 81188e5fd..aaa08fb4a 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -383,6 +383,7 @@ let rec object_type program tenv ot = match ot with | JBasics.TClass cn -> get_class_type program tenv cn | JBasics.TArray at -> Typ.Tptr (Typ.Tarray (value_type program tenv at, None), Typ.Pk_pointer) + (** translate a value type *) and value_type program tenv vt = match vt with diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 8f3c99d02..9f5bcd76a 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -133,7 +133,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) { (ProcAttributes.default proc_name Config.Clang) with ProcAttributes.formals = IList.map (fun (tp, name) -> (Mangled.from_string name, trans_typ tp)) params; - is_defined = true; (** is defined and not just declared *) + is_defined = true; (* is defined and not just declared *) loc = source_only_location (); locals = []; (* TODO *) ret_type;