diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index be40f0883..e61e9b04b 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -594,9 +594,8 @@ module Procname = struct module Java = struct type kind = | Non_Static - (* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface *) - | Static - (* in Java, procedures called with invokestatic *) + (** in Java, procedures called with invokevirtual, invokespecial, and invokeinterface *) + | Static (** in Java, procedures called with invokestatic *) [@@deriving compare] (* TODO: use Mangled.t here *) diff --git a/infer/src/base/SourceFile.ml b/infer/src/base/SourceFile.ml index 860d3fa11..20bcee77d 100644 --- a/infer/src/base/SourceFile.ml +++ b/infer/src/base/SourceFile.ml @@ -15,13 +15,10 @@ let count_newlines (path : string) : int = type t = - | Invalid of string - (* ML function of origin *) + | Invalid of {ml_source_file: string} | Absolute of string - | RelativeProjectRoot of string - (* relative to project root *) - | RelativeInferModel of string - (* relative to infer models *) + | RelativeProjectRoot of string (** relative to project root *) + | RelativeInferModel of string (** relative to infer models *) [@@deriving compare] let equal = [%compare.equal: t] @@ -71,8 +68,8 @@ let to_string = let root = Utils.realpath Config.project_root in fun ?(force_relative = false) fname -> match fname with - | Invalid origin -> - "DUMMY from " ^ origin + | Invalid {ml_source_file} -> + "DUMMY from " ^ ml_source_file | RelativeInferModel path -> "INFER_MODEL/" ^ path | RelativeProjectRoot path -> @@ -87,8 +84,9 @@ let pp fmt fname = Format.pp_print_string fmt (to_string fname) let to_abs_path fname = match fname with - | Invalid origin -> - L.(die InternalError) "cannot be called with Invalid source file originating in %s" origin + | Invalid {ml_source_file} -> + L.(die InternalError) + "cannot be called with Invalid source file originating in %s" ml_source_file | RelativeProjectRoot path -> Filename.concat Config.project_root path | RelativeInferModel path -> @@ -106,14 +104,14 @@ let to_rel_path fname = match fname with RelativeProjectRoot path -> path | _ -> to_abs_path fname -let invalid origin = Invalid origin +let invalid ml_source_file = Invalid {ml_source_file} let is_invalid = function Invalid _ -> true | _ -> false let is_infer_model source_file = match source_file with - | Invalid origin -> - L.(die InternalError) "cannot be called with Invalid source file from %s" origin + | Invalid {ml_source_file} -> + L.(die InternalError) "cannot be called with Invalid source file from %s" ml_source_file | RelativeProjectRoot _ | Absolute _ -> false | RelativeInferModel _ -> @@ -130,8 +128,8 @@ let is_cpp_model file = let is_under_project_root = function - | Invalid origin -> - L.(die InternalError) "cannot be called with Invalid source file from %s" origin + | Invalid {ml_source_file} -> + L.(die InternalError) "cannot be called with Invalid source file from %s" ml_source_file | RelativeProjectRoot _ -> true | Absolute _ | RelativeInferModel _ -> diff --git a/infer/src/biabduction/Absarray.ml b/infer/src/biabduction/Absarray.ml index 63796d328..3fd560ffd 100644 --- a/infer/src/biabduction/Absarray.ml +++ b/infer/src/biabduction/Absarray.ml @@ -62,13 +62,6 @@ module StrexpMatch : sig val replace_index : Tenv.t -> bool -> t -> Exp.t -> Exp.t -> sigma (** Replace the index in the array at a given position with the new index *) - (* - (** Get the partition of the sigma: the unmatched part of the sigma and the matched hpred *) - val get_sigma_partition : t -> sigma * Sil.hpred - - (** Replace the strexp and the unmatched part of the sigma by the givn inputs *) - val replace_strexp_sigma : bool -> t -> Sil.strexp -> sigma -> sigma -*) end = struct (** syntactic offset *) type syn_offset = Field of Typ.Fieldname.t * Typ.t | Index of Exp.t diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml index 1af0ebbc3..ed25eeea2 100644 --- a/infer/src/biabduction/Dom.ml +++ b/infer/src/biabduction/Dom.ml @@ -409,9 +409,6 @@ module FreshVarExp : sig val get_induced_pi : Tenv.t -> unit -> Prop.pi val final : unit -> unit - (* - val lookup : side -> Exp.t -> (Exp.t * Exp.t) option -*) end = struct let t = ref [] diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index badae74a0..a0810ff1d 100644 --- a/infer/src/biabduction/Paths.ml +++ b/infer/src/biabduction/Paths.ml @@ -58,20 +58,12 @@ module Path : sig val start : Procdesc.Node.t -> t (** create a new path with given start node *) - (* - (** equality for paths *) - val equal : t -> t -> bool - - val get_description : t -> string option -*) end = struct type session = int [@@deriving compare] type stats = - { mutable max_length: int - ; (* length of the longest linear sequence *) - mutable linear_num: float - (* number of linear sequences described by the path *) } + { mutable max_length: int (** length of the longest linear sequence *) + ; mutable linear_num: float (** number of linear sequences described by the path *) } (* type aliases for components of t values that compare should ignore *) type stats_ = stats diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 3e0e73de5..da4d2305c 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -261,28 +261,6 @@ module Inequalities : sig val inconsistent : t -> bool (** Return [true] if a simple inconsistency is detected *) - (* - (** Extract inequalities and disequalities from [pi] *) - val from_pi : Sil.atom list -> t - - (** Extract inequalities and disequalities from [sigma] *) - val from_sigma : Sil.hpred list -> t - - (** Join two sets of inequalities *) - val join : t -> t -> t - - (** Pretty print inequalities and disequalities *) - val pp : printenv -> Format.formatter -> t -> unit - - (** Pretty print <= *) - val d_leqs : t -> unit - - (** Pretty print < *) - val d_lts : t -> unit - - (** Pretty print <> *) - val d_neqs : t -> unit -*) end = struct type t = { mutable leqs: (Exp.t * Exp.t) list (** le fasts [e1 <= e2] *) @@ -429,6 +407,7 @@ end = struct saturate {leqs= !leqs; lts= !lts; neqs= !neqs} + (** Extract inequalities and disequalities from [sigma] *) let from_sigma tenv sigma = let lookup = Tenv.lookup tenv in let leqs = ref [] in @@ -472,6 +451,7 @@ end = struct saturate {leqs= !leqs; lts= !lts; neqs= []} + (** Join two sets of inequalities *) let join ineq1 ineq2 = let leqs_new = ineq1.leqs @ ineq2.leqs in let lts_new = ineq1.lts @ ineq2.lts in diff --git a/infer/src/biabduction/SymExecBlocks.mli b/infer/src/biabduction/SymExecBlocks.mli index 090c80771..0cf92da69 100644 --- a/infer/src/biabduction/SymExecBlocks.mli +++ b/infer/src/biabduction/SymExecBlocks.mli @@ -12,7 +12,7 @@ val resolve_method_with_block_args_and_analyze : -> Typ.Procname.t -> (Exp.t * Typ.t) list -> (Summary.t * (Exp.t * Typ.t) list) option -(* [resolve_method_with_block_args_and_analyze caller_pdesc pname args] +(** [resolve_method_with_block_args_and_analyze caller_pdesc pname args] create a copy of the method pname if it is defined and it's called with the correct number of arguments, and some arguments are block closures. The copy is created by adding extra formals for each captured variable, diff --git a/infer/src/clang/cIssue.ml b/infer/src/clang/cIssue.ml index eef652c10..dc984a40e 100644 --- a/infer/src/clang/cIssue.ml +++ b/infer/src/clang/cIssue.ml @@ -10,16 +10,12 @@ open! IStd type mode = On | Off type 'issue_type issue_desc0 = - { issue_type: 'issue_type - ; (* issue type *) - description: string - ; (* Description in the error message *) - mode: mode - ; loc: Location.t - ; (* location in the code *) - severity: Exceptions.severity - ; suggestion: string option - (* an optional suggestion or correction *) } + { issue_type: 'issue_type (** issue type *) + ; description: string (** Description in the error message *) + ; mode: mode + ; loc: Location.t (** location in the code *) + ; severity: Exceptions.severity + ; suggestion: string option (** an optional suggestion or correction *) } type issue_desc = IssueType.t issue_desc0 diff --git a/infer/src/clang/cIssue.mli b/infer/src/clang/cIssue.mli index 608729c42..5c3e744d4 100644 --- a/infer/src/clang/cIssue.mli +++ b/infer/src/clang/cIssue.mli @@ -10,16 +10,12 @@ open! IStd type mode = On | Off type 'issue_type issue_desc0 = - { issue_type: 'issue_type - ; (* issue type *) - description: string - ; (* Description in the error message *) - mode: mode - ; loc: Location.t - ; (* location in the code *) - severity: Exceptions.severity - ; suggestion: string option - (* an optional suggestion or correction *) } + { issue_type: 'issue_type (** issue type *) + ; description: string (** Description in the error message *) + ; mode: mode + ; loc: Location.t (** location in the code *) + ; severity: Exceptions.severity + ; suggestion: string option (** an optional suggestion or correction *) } type issue_desc = IssueType.t issue_desc0 diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 452a84169..ac3ac3132 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -7,10 +7,12 @@ open! IStd open Ctl_parser_types -(* This module defines a language to define checkers. These checkers - are intepreted over the AST of the program. A checker is defined by a - CTL formula which express a condition saying when the checker should - report a problem *) + +(** + This module defines a language to define checkers. These checkers are interpreted over the AST of + the program. A checker is defined by a CTL formula which expresses a condition saying when the + checker should report a problem. +*) (** Transition labels used for example to switch from decl to stmt *) type transitions = @@ -50,18 +52,13 @@ type t = (** EF phi <=> there exits a a path from the current node with a descendant where phi hold *) | AG of transitions option * t (** AG phi <=> for all discendant of the current node phi hold *) | EG of transitions option * t - (** EG phi <=> - there exists a path (of descendants) from the current node where phi hold at each node of the path *) + (** EG phi <=> there exists a path (of descendants) from the current node where phi hold at each node of the path *) | AU of transitions option * t * t - (** AU(phi1, phi2) <=> - for all paths from the current node phi1 holds in every node until ph2 holds *) + (** AU(phi1, phi2) <=> for all paths from the current node phi1 holds in every node until ph2 holds *) | EU of transitions option * t * t - (** EU(phi1, phi2) <=> - there exists a path from the current node such that phi1 holds until phi2 holds *) + (** EU(phi1, phi2) <=> there exists a path from the current node such that phi1 holds until phi2 holds *) | EH of ALVar.alexp list * t - (** EH[classes]phi <=> - there exists a node defining a super class in the hierarchy of the class - defined by the current node (if any) where phi holds *) + (** EH[classes]phi <=> there exists a node defining a super class in the hierarchy of the class defined by the current node (if any) where phi holds *) | ET of ALVar.alexp list * transitions option * t (** ET [T] [l] phi <=> there exists a descentant an of the current node such that an is of type in set T making a transition to a node an' via label l, such that in an phi holds. *) @@ -88,16 +85,13 @@ type t = val equal : t -> t -> bool type clause = - | CLet of ALVar.formula_id * ALVar.t list * t - (* Let clause: let id = definifion; *) - | CSet of ALVar.keyword * t - (* Set clause: set id = definition *) - | CDesc of ALVar.keyword * string - (* Description clause eg: set message = "..." *) + | CLet of ALVar.formula_id * ALVar.t list * t (** Let clause: let id = definifion; *) + | CSet of ALVar.keyword * t (** Set clause: set id = definition *) + | CDesc of ALVar.keyword * string (** Description clause eg: set message = "..." *) | CPath of [`WhitelistPath | `BlacklistPath] * ALVar.t list type ctl_checker = - {id: string; (* Checker's id *) definitions: clause list (* A list of let/set definitions *)} + {id: string (** Checker's id *); definitions: clause list (** A list of let/set definitions *)} type al_file = { import_files: string list diff --git a/infer/src/nullsafe/eradicate.mli b/infer/src/nullsafe/eradicate.mli index e8327a26b..530281efc 100644 --- a/infer/src/nullsafe/eradicate.mli +++ b/infer/src/nullsafe/eradicate.mli @@ -17,7 +17,6 @@ val callback_check_return_type : TypeCheck.check_return_type -> Callbacks.proc_c module type CallBackT = sig val callback : TypeCheck.checks -> Callbacks.proc_callback_t end -(* CallBackT *) (** Extension to the type checker. *) module type ExtensionT = sig