From 65f369cf35aa718edf876a1c7f13f3ff1ecc7c62 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 16 May 2020 08:28:37 -0700 Subject: [PATCH] [ocamlformat] Reformat repo with new version Reviewed By: jvillard Differential Revision: D21583046 fbshipit-source-id: ee4793880 --- infer/src/IR/Exp.mli | 6 +++--- infer/src/IR/Fieldname.mli | 4 ++-- infer/src/IR/Ident.mli | 6 +++--- infer/src/IR/Mangled.mli | 4 ++-- infer/src/IR/Procdesc.ml | 8 ++++---- infer/src/IR/Procdesc.mli | 10 +++++----- infer/src/IR/Procname.mli | 6 +++--- infer/src/IR/Pvar.mli | 2 +- infer/src/IR/Tenv.ml | 2 +- infer/src/IR/WeakTopologicalOrder.ml | 2 +- infer/src/IR/WeakTopologicalOrder.mli | 2 +- infer/src/absint/AbstractDomain.mli | 12 ++++++------ infer/src/absint/AbstractInterpreter.ml | 3 +-- infer/src/absint/AbstractInterpreter.mli | 4 ++-- infer/src/absint/AccessTree.mli | 2 +- infer/src/absint/ExplicitTrace.mli | 6 +++--- infer/src/absint/TaintTrace.mli | 8 ++++---- infer/src/absint/TaskSchedulerTypes.ml | 2 +- infer/src/absint/TransferFunctions.mli | 2 +- infer/src/al/CTLExceptions.mli | 4 ++-- infer/src/al/ctl_parser_types.ml | 6 ++---- infer/src/backend/Payloads.ml | 3 +-- infer/src/backend/preanal.ml | 2 +- infer/src/base/CommandLineOption.ml | 2 +- infer/src/base/Die.mli | 2 +- infer/src/base/ResultsDir.ml | 3 +-- infer/src/base/SourceFile.mli | 4 ++-- infer/src/base/SqliteUtils.mli | 2 +- infer/src/base/SymOp.ml | 2 +- infer/src/base/SymOp.mli | 2 +- infer/src/biabduction/BiabductionSummary.mli | 2 +- infer/src/biabduction/BuiltinDefn.mli | 2 +- infer/src/biabduction/Predicates.mli | 2 +- infer/src/biabduction/RetainCyclesType.mli | 2 +- infer/src/bufferoverrun/bufferOverrunDomain.mli | 2 +- infer/src/bufferoverrun/bufferOverrunModels.ml | 3 ++- infer/src/bufferoverrun/polynomials.ml | 7 ++++--- infer/src/checkers/LithoDomain.ml | 2 +- infer/src/checkers/classLoads.ml | 3 ++- infer/src/checkers/control.ml | 6 +++--- infer/src/checkers/control.mli | 6 +++--- infer/src/checkers/loopInvariant.ml | 4 ++-- infer/src/checkers/loopInvariant.mli | 4 ++-- infer/src/checkers/reachingDefs.ml | 4 ++-- infer/src/checkers/reachingDefs.mli | 4 ++-- infer/src/checkers/uninit.ml | 2 +- infer/src/clang/cFrontend.ml | 3 +-- infer/src/clang/cTrans.ml | 4 ++-- infer/src/concurrency/starvationDomain.ml | 4 ++-- infer/src/cost/hoisting.ml | 2 +- infer/src/integration/Differential.ml | 3 +-- infer/src/integration/JsonReports.ml | 3 +-- infer/src/java/jContext.mli | 2 +- infer/src/labs/00_dummy_checker/ResourceLeaks.ml | 2 +- infer/src/labs/01_integer_domain/ResourceLeaks.ml | 2 +- infer/src/labs/02_domain_join/ResourceLeaks.ml | 2 +- infer/src/labs/03_domain_top/ResourceLeaks.ml | 2 +- infer/src/labs/04_interprocedural/ResourceLeaks.ml | 2 +- .../05_access_paths_interprocedural/ResourceLeaks.ml | 2 +- infer/src/labs/ResourceLeaks.ml | 2 +- infer/src/nullsafe/Initializers.ml | 3 +-- infer/src/nullsafe/unit/AggregatedSummariesTest.ml | 3 +-- infer/src/pulse/PulseAbductiveDomain.ml | 3 ++- infer/src/pulse/PulseAbductiveDomain.mli | 4 ++-- infer/src/pulse/PulseDomainInterface.ml | 4 ++-- infer/src/pulse/PulseOperations.ml | 6 ++---- infer/src/pulse/PulsePathCondition.ml | 4 ++-- infer/src/quandary/TaintAnalysis.ml | 3 +-- infer/src/unit/LRUHashtblTests.ml | 3 +-- sledge/bin/frontend.ml | 2 +- sledge/src/equality.ml | 9 +++------ sledge/src/sh.ml | 4 ++-- sledge/src/term.mli | 6 +++--- 73 files changed, 127 insertions(+), 140 deletions(-) diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli index 43901103c..0b332f64e 100644 --- a/infer/src/IR/Exp.mli +++ b/infer/src/IR/Exp.mli @@ -46,14 +46,14 @@ and t = val equal : t -> t -> bool (** Equality for expressions. *) -module Set : Caml.Set.S with type elt = t (** Set of expressions. *) +module Set : Caml.Set.S with type elt = t -module Map : Caml.Map.S with type key = t (** Map with expression keys. *) +module Map : Caml.Map.S with type key = t -module Hash : Caml.Hashtbl.S with type key = t (** Hashtable with expression keys. *) +module Hash : Caml.Hashtbl.S with type key = t val is_null_literal : t -> bool diff --git a/infer/src/IR/Fieldname.mli b/infer/src/IR/Fieldname.mli index 830c36911..22de15723 100644 --- a/infer/src/IR/Fieldname.mli +++ b/infer/src/IR/Fieldname.mli @@ -20,11 +20,11 @@ val get_field_name : t -> string val is_java : t -> bool -module Set : Caml.Set.S with type elt = t (** Set for fieldnames *) +module Set : Caml.Set.S with type elt = t -module Map : Caml.Map.S with type key = t (** Map for fieldnames *) +module Map : Caml.Map.S with type key = t val is_java_outer_instance : t -> bool (** Check if the field is the synthetic this$n of a nested class, used to access the n-th outer diff --git a/infer/src/IR/Ident.mli b/infer/src/IR/Ident.mli index fb3d413f7..571d094dc 100644 --- a/infer/src/IR/Ident.mli +++ b/infer/src/IR/Ident.mli @@ -28,14 +28,14 @@ type kind [@@deriving compare] val equal_kind : kind -> kind -> bool (** Equality for kind. *) -module Set : Caml.Set.S with type elt = t (** Set for identifiers. *) +module Set : Caml.Set.S with type elt = t -module Hash : Caml.Hashtbl.S with type key = t (** Hash table with ident as key. *) +module Hash : Caml.Hashtbl.S with type key = t -module Map : Caml.Map.S with type key = t (** Map with ident as key. *) +module Map : Caml.Map.S with type key = t module HashQueue : Hash_queue.S with type key = t diff --git a/infer/src/IR/Mangled.mli b/infer/src/IR/Mangled.mli index fcf27a02c..994657d6a 100644 --- a/infer/src/IR/Mangled.mli +++ b/infer/src/IR/Mangled.mli @@ -42,8 +42,8 @@ val is_self : t -> bool val rename : f:(string -> string) -> t -> t (** Maps over both the plain and the mangled components. *) -module Set : Caml.Set.S with type elt = t (** Set of Mangled. *) +module Set : Caml.Set.S with type elt = t -module Map : Caml.Map.S with type key = t (** Map with Mangled as key *) +module Map : Caml.Map.S with type key = t diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 9e2e060ae..825414438 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -420,17 +420,17 @@ end (* =============== END of module Node =============== *) -module NodeMap = Caml.Map.Make (Node) (** Map over nodes *) +module NodeMap = Caml.Map.Make (Node) -module NodeHash = Hashtbl.Make (Node) (** Hash table with nodes as keys. *) +module NodeHash = Hashtbl.Make (Node) -module NodeSet = Node.NodeSet (** Set of nodes. *) +module NodeSet = Node.NodeSet -module IdMap = Node.IdMap (** Map with node id keys. *) +module IdMap = Node.IdMap (** procedure description *) type t = diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 3e2ca6e22..ef3c7b3c7 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -176,17 +176,17 @@ module Node : sig val compute_key : t -> NodeKey.t end -module IdMap : PrettyPrintable.PPMap with type key = Node.id (** Map with node id keys. *) +module IdMap : PrettyPrintable.PPMap with type key = Node.id -module NodeHash : Caml.Hashtbl.S with type key = Node.t (** Hash table with nodes as keys. *) +module NodeHash : Caml.Hashtbl.S with type key = Node.t -module NodeMap : Caml.Map.S with type key = Node.t (** Map over nodes. *) +module NodeMap : Caml.Map.S with type key = Node.t -module NodeSet : Caml.Set.S with type elt = Node.t (** Set of nodes. *) +module NodeSet : Caml.Set.S with type elt = Node.t (** procedure descriptions *) @@ -310,8 +310,8 @@ val is_captured_var : t -> Var.t -> bool val has_modify_in_block_attr : t -> Pvar.t -> bool -module SQLite : SqliteUtils.Data with type t = t option (** per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no CFG *) +module SQLite : SqliteUtils.Data with type t = t option val load : Procname.t -> t option diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli index d450ab6c2..242d5df75 100644 --- a/infer/src/IR/Procname.mli +++ b/infer/src/IR/Procname.mli @@ -224,18 +224,18 @@ val is_java_autogen_method : t -> bool val is_objc_method : t -> bool -module Hash : Caml.Hashtbl.S with type key = t (** Hash tables with proc names as keys. *) +module Hash : Caml.Hashtbl.S with type key = t module LRUHash : LRUHashtbl.S with type key = t module HashQueue : Hash_queue.S with type key = t -module Map : PrettyPrintable.PPMap with type key = t (** Maps from proc names. *) +module Map : PrettyPrintable.PPMap with type key = t -module Set : PrettyPrintable.PPSet with type elt = t (** Sets of proc names. *) +module Set : PrettyPrintable.PPSet with type elt = t module SQLite : sig val serialize : t -> Sqlite3.Data.t diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index 3cd26dd61..370b000cf 100644 --- a/infer/src/IR/Pvar.mli +++ b/infer/src/IR/Pvar.mli @@ -169,5 +169,5 @@ val materialized_cpp_temporary : string val rename : f:(string -> string) -> t -> t -module Set : PrettyPrintable.PPSet with type elt = t (** Sets of pvars. *) +module Set : PrettyPrintable.PPSet with type elt = t diff --git a/infer/src/IR/Tenv.ml b/infer/src/IR/Tenv.ml index a96c5154b..8ed42642f 100644 --- a/infer/src/IR/Tenv.ml +++ b/infer/src/IR/Tenv.ml @@ -9,8 +9,8 @@ module L = Logging (** Module for Type Environments. *) -module TypenameHash = Caml.Hashtbl.Make (Typ.Name) (** Hash tables on type names. *) +module TypenameHash = Caml.Hashtbl.Make (Typ.Name) module TypenameHashNormalizer = MaximumSharing.ForHashtbl (TypenameHash) diff --git a/infer/src/IR/WeakTopologicalOrder.ml b/infer/src/IR/WeakTopologicalOrder.ml index d43e7228f..04c30e055 100644 --- a/infer/src/IR/WeakTopologicalOrder.ml +++ b/infer/src/IR/WeakTopologicalOrder.ml @@ -111,10 +111,10 @@ module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG module Bourdoncle_SCC (CFG : PreProcCfg) = struct module CFG = CFG - module Dfn = CFG.Node.IdMap (** [dfn] contains a DFS pre-order indexing. A node is not in the map if it has never been visited. A node's dfn is +oo if it has been fully visited (head of cross-edges) or we want to hide it for building a subcomponent partition (head of highest back-edges). *) + module Dfn = CFG.Node.IdMap (* Unlike Bourdoncle's paper version or OCamlGraph implementation, this implementation handles diff --git a/infer/src/IR/WeakTopologicalOrder.mli b/infer/src/IR/WeakTopologicalOrder.mli index a5a8c81d7..cadbba42a 100644 --- a/infer/src/IR/WeakTopologicalOrder.mli +++ b/infer/src/IR/WeakTopologicalOrder.mli @@ -74,6 +74,6 @@ end module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG -module Bourdoncle_SCC : Make (** Implementation of Bourdoncle's "Hierarchical decomposition of a directed graph into strongly connected components and subcomponents". See [Bou] Figure 4, page 10. *) +module Bourdoncle_SCC : Make diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 9aefc483a..4691c8055 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -38,8 +38,8 @@ include (* ocaml ignores the warning suppression at toplevel, hence the [include sig [@@@warning "-60"] - module Empty : S with type t = unit (** a trivial domain *) + module Empty : S with type t = unit end (** A domain with an explicit bottom value *) @@ -253,13 +253,13 @@ include sig end end -module BooleanAnd : S with type t = bool (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's true in both conditional branches. *) +module BooleanAnd : S with type t = bool -module BooleanOr : WithBottom with type t = bool (** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's true in one conditional branch. *) +module BooleanOr : WithBottom with type t = bool module type MaxCount = sig val max : int @@ -271,8 +271,8 @@ end module CountDomain (MaxCount : MaxCount) : sig include WithBottom with type t = private int - include WithTop with type t := t (** top is maximum value *) + include WithTop with type t := t val increment : t -> t (** bump the count by one if it is less than the max *) @@ -287,11 +287,11 @@ end (** Domain keeping a non-negative count with a bounded maximum value. [join] is minimum and [top] is zero. *) module DownwardIntDomain (MaxCount : MaxCount) : sig - include WithTop with type t = private int (** top is zero *) + include WithTop with type t = private int - include WithBottom with type t := t (** bottom is the provided maximum *) + include WithBottom with type t := t val increment : t -> t (** bump the count by one if this won't cross the maximum *) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 3922a3a29..4883aea20 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -402,8 +402,7 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s (* shadowed for HTML debug *) let compute_pre cfg node inv_map = AnalysisCallbacks.html_debug_new_node_session (Node.underlying_node node) ~kind:`ComputePre - ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map - ) + ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map) (** compute and return an invariant map for [pdesc] *) diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index 5370c02d4..c6fceff6e 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -63,13 +63,13 @@ end module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S with module TransferFunctions = TransferFunctions -module MakeRPO : Make (** create an intraprocedural abstract interpreter from transfer functions using the reverse post-order scheduler *) +module MakeRPO : Make -module MakeWTO : Make (** create an intraprocedural abstract interpreter from transfer functions using Bourdoncle's strongly connected component weak topological order *) +module MakeWTO : Make (** In the disjunctive interpreter, the domain is a set of abstract states representing a disjunction between these states. The transfer functions are executed on each state in the diff --git a/infer/src/absint/AccessTree.mli b/infer/src/absint/AccessTree.mli index 25b499237..f784fd180 100644 --- a/infer/src/absint/AccessTree.mli +++ b/infer/src/absint/AccessTree.mli @@ -22,7 +22,6 @@ module type S = sig (** map from access -> nodes. a leaf is encoded as an empty map *) | Star (** special leaf for starred access paths *) - include AbstractDomain.WithBottom with type t = node BaseMap.t (** map from base var -> access subtree. Here's how to represent a few different kinds of trace * access path associations: @@ -35,6 +34,7 @@ module type S = sig (x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}), g |-> (T2, Subtree {}) }) } ]} *) + include AbstractDomain.WithBottom with type t = node BaseMap.t val empty_node : node diff --git a/infer/src/absint/ExplicitTrace.mli b/infer/src/absint/ExplicitTrace.mli index 3c190d664..e67958681 100644 --- a/infer/src/absint/ExplicitTrace.mli +++ b/infer/src/absint/ExplicitTrace.mli @@ -24,8 +24,8 @@ end module type CallPrinter = PrettyPrintable.PrintableType with type t = CallSite.t -module DefaultCallPrinter : CallPrinter (** Printer which outputs "Method call: " *) +module DefaultCallPrinter : CallPrinter module type TraceElem = sig type elem_t @@ -33,8 +33,8 @@ module type TraceElem = sig (** An [elem] which occured at [loc], after the chain of steps (usually calls) in [trace]. *) type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list} - include Element with type t := t (** Both [pp] and [describe] simply call the same function on the trace element. *) + include Element with type t := t val make : elem_t -> Location.t -> t @@ -48,8 +48,8 @@ module type TraceElem = sig val with_callsite : t -> CallSite.t -> t (** Push given callsite onto trace, extending the call chain by one. *) - module FiniteSet : FiniteSet with type elt = t (** A powerset of traces. *) + module FiniteSet : FiniteSet with type elt = t end (* The [compare] function produced ignores traces but *not* locations *) diff --git a/infer/src/absint/TaintTrace.mli b/infer/src/absint/TaintTrace.mli index a72c3e6c6..6f16f9195 100644 --- a/infer/src/absint/TaintTrace.mli +++ b/infer/src/absint/TaintTrace.mli @@ -23,20 +23,20 @@ end module type S = sig include Spec - include AbstractDomain.WithBottom (** bottom = this trace has no source or sink data *) + include AbstractDomain.WithBottom module Sources : sig - module Known : module type of AbstractDomain.FiniteSet (Source) (** Set of sources returned by callees of the current function *) + module Known : module type of AbstractDomain.FiniteSet (Source) module FootprintConfig : AccessTree.Config - module Footprint : module type of AccessTree.PathSet (FootprintConfig) (** Set of access paths representing the sources that may flow in from the caller *) + module Footprint : module type of AccessTree.PathSet (FootprintConfig) - module Sanitizers : module type of AbstractDomain.FiniteSet (Sanitizer) (** Set of sanitizers that have been applied to these sources *) + module Sanitizers : module type of AbstractDomain.FiniteSet (Sanitizer) type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t} diff --git a/infer/src/absint/TaskSchedulerTypes.ml b/infer/src/absint/TaskSchedulerTypes.ml index 4550df667..304da6d2a 100644 --- a/infer/src/absint/TaskSchedulerTypes.ml +++ b/infer/src/absint/TaskSchedulerTypes.ml @@ -6,8 +6,8 @@ *) open! IStd -exception ProcnameAlreadyLocked of Procname.t (** for the Restart scheduler: raise when a worker tries to analyze a procedure already being analyzed by another process *) +exception ProcnameAlreadyLocked of Procname.t type target = Procname of Procname.t | File of SourceFile.t diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 3b86b3e83..6c99c7805 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -13,8 +13,8 @@ open! IStd module type S = sig module CFG : ProcCfg.S - module Domain : AbstractDomain.S (** abstract domain whose state we propagate *) + module Domain : AbstractDomain.S (** read-only extra state (results of previous analyses, globals, etc.) *) type analysis_data diff --git a/infer/src/al/CTLExceptions.mli b/infer/src/al/CTLExceptions.mli index cccd15fce..d3e70019b 100644 --- a/infer/src/al/CTLExceptions.mli +++ b/infer/src/al/CTLExceptions.mli @@ -7,13 +7,13 @@ open! IStd -exception ALParserInvariantViolationException of string (** Raised when the parser encounters a violation of a certain invariant *) +exception ALParserInvariantViolationException of string type exc_info -exception ALFileException of exc_info (** Raised when any exception from the lexer/parser of AL is caught, to include source-location info *) +exception ALFileException of exc_info val create_exc_info : string -> Lexing.lexbuf -> exc_info diff --git a/infer/src/al/ctl_parser_types.ml b/infer/src/al/ctl_parser_types.ml index 853591659..93c607973 100644 --- a/infer/src/al/ctl_parser_types.ml +++ b/infer/src/al/ctl_parser_types.ml @@ -231,13 +231,11 @@ let rec is_node_successor_of ~is_successor:succ_node node = | Stmt _ -> let node_succ_stmts = get_successor_stmts node in List.exists node_succ_stmts ~f:(fun (s : Clang_ast_t.stmt) -> - ast_node_equal (Stmt s) succ_node || is_node_successor_of ~is_successor:succ_node (Stmt s) - ) + ast_node_equal (Stmt s) succ_node || is_node_successor_of ~is_successor:succ_node (Stmt s) ) | Decl _ -> let node_succ_decls = get_successor_decls node in List.exists node_succ_decls ~f:(fun (d : Clang_ast_t.decl) -> - ast_node_equal (Decl d) succ_node || is_node_successor_of ~is_successor:succ_node (Decl d) - ) + ast_node_equal (Decl d) succ_node || is_node_successor_of ~is_successor:succ_node (Decl d) ) let get_direct_successor_nodes an = diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 34c210274..60555d621 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -55,8 +55,7 @@ let fields = let pp pe f payloads = List.iter fields ~f:(fun (F {field; name; pp}) -> - Field.get field payloads |> Option.iter ~f:(fun x -> F.fprintf f "%s: %a@\n" name (pp pe) x) - ) + Field.get field payloads |> Option.iter ~f:(fun x -> F.fprintf f "%s: %a@\n" name (pp pe) x) ) let empty = diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 12b3fe69a..3c79d13fb 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -156,8 +156,8 @@ module Liveness = struct instructions for each pvar in to_nullify afer we finish the analysis. Nullify instructions speed up the analysis by enabling it to GC state that will no longer be read. *) module NullifyTransferFunctions = struct - module Domain = AbstractDomain.Pair (VarDomain) (VarDomain) (** (reaching non-nullified vars) * (vars to nullify) *) + module Domain = AbstractDomain.Pair (VarDomain) (VarDomain) module CFG = ProcCfg.Exceptional diff --git a/infer/src/base/CommandLineOption.ml b/infer/src/base/CommandLineOption.ml index 2fa04596c..630604a5e 100644 --- a/infer/src/base/CommandLineOption.ml +++ b/infer/src/base/CommandLineOption.ml @@ -592,7 +592,7 @@ let normalize_path_in_args_being_parsed ?(f = Fn.id) ~is_anon_arg str = [Arg.parse_argv_dynamic ~current:arg_being_parsed !args_to_parse ...]. *) let root = Unix.getcwd () in let abs_path = Utils.filename_to_absolute ~root str in - !args_to_parse.((!arg_being_parsed + if is_anon_arg then 0 else 1)) <- f abs_path ; + !args_to_parse.(!arg_being_parsed + if is_anon_arg then 0 else 1) <- f abs_path ; abs_path ) else str diff --git a/infer/src/base/Die.mli b/infer/src/base/Die.mli index daa0b4b3b..d0242f3a2 100644 --- a/infer/src/base/Die.mli +++ b/infer/src/base/Die.mli @@ -16,8 +16,8 @@ exception InferInternalError of string exception InferUserError of string -exception InferExit of int (** This can be used to avoid scattering exit invocations all over the codebase *) +exception InferExit of int (** kind of error for [die], with similar semantics as [Logging.{external,internal,user}_error] *) type error = ExternalError | InternalError | UserError diff --git a/infer/src/base/ResultsDir.ml b/infer/src/base/ResultsDir.ml index 836032c44..4c3ad7860 100644 --- a/infer/src/base/ResultsDir.ml +++ b/infer/src/base/ResultsDir.ml @@ -134,8 +134,7 @@ let create_results_dir () = L.progress "Deleting results dir because --force-delete-results-dir was passed@." ; remove_results_dir () ) else - L.die UserError "ERROR: %s@\nPlease remove '%s' and try again" error Config.results_dir - ) ; + L.die UserError "ERROR: %s@\nPlease remove '%s' and try again" error Config.results_dir ) ; Unix.mkdir_p Config.results_dir ; Unix.mkdir_p (get_path Temporary) ; Unix.mkdir_p (get_path Specs) ; diff --git a/infer/src/base/SourceFile.mli b/infer/src/base/SourceFile.mli index c387c1c41..8e01d5ed3 100644 --- a/infer/src/base/SourceFile.mli +++ b/infer/src/base/SourceFile.mli @@ -9,11 +9,11 @@ open! IStd type t [@@deriving compare] -module Map : Caml.Map.S with type key = t (** Maps from source_file *) +module Map : Caml.Map.S with type key = t -module Set : Caml.Set.S with type elt = t (** Set of source files *) +module Set : Caml.Set.S with type elt = t module Hash : Caml.Hashtbl.S with type key = t diff --git a/infer/src/base/SqliteUtils.mli b/infer/src/base/SqliteUtils.mli index 375e21f3d..f9bad45e4 100644 --- a/infer/src/base/SqliteUtils.mli +++ b/infer/src/base/SqliteUtils.mli @@ -7,9 +7,9 @@ open! IStd -exception Error of string (** The functions in this module tend to raise more often than their counterparts in [Sqlite3]. In particular, they may raise if the [Sqlite3.Rc.t] result of certain operations is unexpected. *) +exception Error of string val check_result_code : Sqlite3.db -> log:string -> Sqlite3.Rc.t -> unit (** Assert that the result is either [Sqlite3.Rc.OK] or [Sqlite3.Rc.ROW]. If the result is not diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index 47c4dba2f..dde00954f 100644 --- a/infer/src/base/SymOp.ml +++ b/infer/src/base/SymOp.ml @@ -17,8 +17,8 @@ type failure_kind = | FKrecursion_timeout of int (** max recursion level exceeded *) | FKcrash of string (** uncaught exception or failed assertion *) -exception Analysis_failure_exe of failure_kind (** failure that prevented analysis from finishing *) +exception Analysis_failure_exe of failure_kind let exn_not_failure = function Analysis_failure_exe _ -> false | _ -> true diff --git a/infer/src/base/SymOp.mli b/infer/src/base/SymOp.mli index 215505a9a..7851e9531 100644 --- a/infer/src/base/SymOp.mli +++ b/infer/src/base/SymOp.mli @@ -59,8 +59,8 @@ type failure_kind = | FKrecursion_timeout of int (** max recursion level exceeded *) | FKcrash of string (** uncaught exception or failed assertion *) -exception Analysis_failure_exe of failure_kind (** Timeout exception *) +exception Analysis_failure_exe of failure_kind val exn_not_failure : exn -> bool (** check that the exception is not a timeout exception *) diff --git a/infer/src/biabduction/BiabductionSummary.mli b/infer/src/biabduction/BiabductionSummary.mli index 3f8495dc5..1848eb0dc 100644 --- a/infer/src/biabduction/BiabductionSummary.mli +++ b/infer/src/biabduction/BiabductionSummary.mli @@ -44,8 +44,8 @@ module Jprop : sig (** Extract the toplevel jprop of a prop *) end -module Visitedset : Caml.Set.S with type elt = Procdesc.Node.id * int list (** set of visited nodes: node id and list of lines of all the instructions *) +module Visitedset : Caml.Set.S with type elt = Procdesc.Node.id * int list (** A spec consists of: diff --git a/infer/src/biabduction/BuiltinDefn.mli b/infer/src/biabduction/BuiltinDefn.mli index d71ca847b..b5c7a2a8c 100644 --- a/infer/src/biabduction/BuiltinDefn.mli +++ b/infer/src/biabduction/BuiltinDefn.mli @@ -7,8 +7,8 @@ open! IStd -include BUILTINS.S with type t = Builtin.registered (** Models for the builtin functions supported *) +include BUILTINS.S with type t = Builtin.registered val init : unit -> unit (** Clients of Builtin module should call this before Builtin module is used. WARNING: builtins are diff --git a/infer/src/biabduction/Predicates.mli b/infer/src/biabduction/Predicates.mli index 2c3e17561..ecf33ef1a 100644 --- a/infer/src/biabduction/Predicates.mli +++ b/infer/src/biabduction/Predicates.mli @@ -161,8 +161,8 @@ val equal_hpred : ?inst:bool -> hpred -> hpred -> bool (** Equality function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default). *) -module HpredSet : Caml.Set.S with type elt = hpred (** Sets of heap predicates *) +module HpredSet : Caml.Set.S with type elt = hpred (** {2 Compaction} *) diff --git a/infer/src/biabduction/RetainCyclesType.mli b/infer/src/biabduction/RetainCyclesType.mli index 49d1452bf..ccfd1d60a 100644 --- a/infer/src/biabduction/RetainCyclesType.mli +++ b/infer/src/biabduction/RetainCyclesType.mli @@ -19,8 +19,8 @@ type retain_cycle_edge = Object of retain_cycle_edge_obj | Block of Procname.t * to model the cycle structure. The next element from the end of the list is the head. *) type t = {rc_head: retain_cycle_edge; rc_elements: retain_cycle_edge list} -module Set : Caml.Set.S with type elt = t (** Set for retain cycles. *) +module Set : Caml.Set.S with type elt = t val d_retain_cycle : t -> unit diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 989b160d0..0de65705d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -8,8 +8,8 @@ open! IStd open AbstractDomain.Types -module ItvThresholds : AbstractDomain.FiniteSetS with type elt = Z.t (** Set of integers for threshold widening *) +module ItvThresholds : AbstractDomain.FiniteSetS with type elt = Z.t (** Domain for recording which operations are used for evaluating interval values *) module ItvUpdatedBy : sig diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index c2e0cacf1..a1b150f02 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -627,7 +627,8 @@ module StdVector = struct let set_size {location} locs new_size mem = - Dom.Mem.transform_mem locs mem ~f:(fun v -> Dom.Val.set_array_length location ~length:new_size v) + Dom.Mem.transform_mem locs mem ~f:(fun v -> + Dom.Val.set_array_length location ~length:new_size v ) let empty elt_typ vec_arg = diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 939f6bcc8..88242c721 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -305,8 +305,8 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct (fun symbol polynomial acc -> Option.bind acc ~f:(fun acc -> Option.bind (S.int_ub symbol) ~f:(fun s_ub -> - Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc)) - ) ) ) + Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc)) ) ) + ) terms (Some const) @@ -315,7 +315,8 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct fun ~lhs ~rhs -> phys_equal lhs rhs || (NonNegativeInt.leq ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:leq lhs.terms rhs.terms) - || Option.exists (int_ub lhs) ~f:(fun lhs_ub -> NonNegativeInt.leq ~lhs:lhs_ub ~rhs:(int_lb rhs)) + || Option.exists (int_ub lhs) ~f:(fun lhs_ub -> + NonNegativeInt.leq ~lhs:lhs_ub ~rhs:(int_lb rhs) ) let rec xcompare ~lhs ~rhs = diff --git a/infer/src/checkers/LithoDomain.ml b/infer/src/checkers/LithoDomain.ml index 2c1dba430..77cfb9620 100644 --- a/infer/src/checkers/LithoDomain.ml +++ b/infer/src/checkers/LithoDomain.ml @@ -138,8 +138,8 @@ module Created = struct end module MethodCalls = struct - module IsChecked = AbstractDomain.BooleanOr (** if the method calls are checked and reported *) + module IsChecked = AbstractDomain.BooleanOr module S = AbstractDomain.InvertedSet (MethodCallPrefix) diff --git a/infer/src/checkers/classLoads.ml b/infer/src/checkers/classLoads.ml index 6ff039601..2a107771f 100644 --- a/infer/src/checkers/classLoads.ml +++ b/infer/src/checkers/classLoads.ml @@ -87,7 +87,8 @@ let exec_call analysis_data callee args loc astate = load_type analysis_data loc typ astate | _ -> (* invokeinterface / invokespecial / invokestatic / invokevirtual / new *) - List.fold args ~init:astate ~f:(fun acc (exp, _) -> add_loads_of_exp analysis_data loc exp acc) + List.fold args ~init:astate ~f:(fun acc (exp, _) -> + add_loads_of_exp analysis_data loc exp acc ) |> do_call analysis_data callee loc diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index d31eb054e..9cae77b76 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -35,17 +35,17 @@ end module ControlDepSet = AbstractDomain.FiniteSet (CVar) -module ControlMap = PrettyPrintable.MakePPMap (Var) (** Map control var -> loop head location *) +module ControlMap = PrettyPrintable.MakePPMap (Var) module GuardNodes = AbstractDomain.FiniteSet (Procdesc.Node) module LoopHeads = Procdesc.NodeSet -module ExitNodeToLoopHeads = Procdesc.NodeMap (** Map exit node -> loop head set *) +module ExitNodeToLoopHeads = Procdesc.NodeMap -module LoopHeadToGuardNodes = Procdesc.NodeMap (** Map loop head -> prune nodes in the loop guard *) +module LoopHeadToGuardNodes = Procdesc.NodeMap type loop_control_maps = { exit_map: LoopHeads.t ExitNodeToLoopHeads.t diff --git a/infer/src/checkers/control.mli b/infer/src/checkers/control.mli index d0e1e455e..dc7df0fdb 100644 --- a/infer/src/checkers/control.mli +++ b/infer/src/checkers/control.mli @@ -9,16 +9,16 @@ open! IStd module LoopHead = Procdesc.Node module LoopHeads = Procdesc.NodeSet -module ControlMap : module type of PrettyPrintable.MakePPMap (Var) (** Map control var -> loop head location *) +module ControlMap : module type of PrettyPrintable.MakePPMap (Var) module GuardNodes : module type of AbstractDomain.FiniteSet (Procdesc.Node) -module ExitNodeToLoopHeads = Procdesc.NodeMap (** Map exit node -> loop head set *) +module ExitNodeToLoopHeads = Procdesc.NodeMap -module LoopHeadToGuardNodes = Procdesc.NodeMap (** Map loop head -> prune nodes in the loop guard *) +module LoopHeadToGuardNodes = Procdesc.NodeMap type invariant_map diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index efdfd2208..f553632ec 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -14,8 +14,8 @@ module VarSet = AbstractDomain.FiniteSet (Var) let debug fmt = L.(debug Analysis Medium) fmt -module LoopHeadToLoopNodes = Procdesc.NodeMap (** Map loop header node -> all nodes in the loop *) +module LoopHeadToLoopNodes = Procdesc.NodeMap let is_defined_outside loop_nodes reaching_defs var = ReachingDefs.ReachingDefsMap.find_opt var reaching_defs @@ -260,8 +260,8 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_pure_by_default ~g find_fixpoint InvariantVars.empty -module LoopHeadToInvVars = Procdesc.NodeMap (** Map loop head -> invariant vars in loop *) +module LoopHeadToInvVars = Procdesc.NodeMap type invariant_map = VarSet.t LoopHeadToInvVars.t diff --git a/infer/src/checkers/loopInvariant.mli b/infer/src/checkers/loopInvariant.mli index a6c25c245..c1142fd9a 100644 --- a/infer/src/checkers/loopInvariant.mli +++ b/infer/src/checkers/loopInvariant.mli @@ -15,11 +15,11 @@ module LoopNodes : module type of AbstractDomain.FiniteSet (Procdesc.Node) module VarSet : module type of AbstractDomain.FiniteSet (Var) -module LoopHeadToLoopNodes = Procdesc.NodeMap (** Map loop header node -> all nodes in the loop *) +module LoopHeadToLoopNodes = Procdesc.NodeMap -module LoopHeadToInvVars = Procdesc.NodeMap (** Map loop head -> invariant vars in loop *) +module LoopHeadToInvVars = Procdesc.NodeMap type invariant_map = VarsInLoop.t Procdesc.NodeMap.t diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index 61ee86d86..b329fc126 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -8,16 +8,16 @@ open! IStd module F = Format module NodeCFG = ProcCfg.Normal -module Defs = AbstractDomain.FiniteSet (Procdesc.Node) (** The node in which the reaching definition x := e is defined. A definition x :=e, declared at node N, reaches the current node if there is a path from node N to the current node such that x is not modified along the path **) +module Defs = AbstractDomain.FiniteSet (Procdesc.Node) (* even though we only add singletons (defs), the set is needed for joins *) -module ReachingDefsMap = AbstractDomain.Map (Var) (Defs) (** Map var -> its reaching definition *) +module ReachingDefsMap = AbstractDomain.Map (Var) (Defs) (* forward transfer function for reaching definitions *) module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct diff --git a/infer/src/checkers/reachingDefs.mli b/infer/src/checkers/reachingDefs.mli index 7aa6bceb6..9687636f4 100644 --- a/infer/src/checkers/reachingDefs.mli +++ b/infer/src/checkers/reachingDefs.mli @@ -7,14 +7,14 @@ open! IStd -module Defs : module type of AbstractDomain.FiniteSet (Procdesc.Node) (** The node in which the reaching definition x := e is defined. A definition x :=e, declared at node N, reaches the current node if there is a path from node N to the current node such that x is not modified along the path **) +module Defs : module type of AbstractDomain.FiniteSet (Procdesc.Node) -module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs) (** Map var -> its reaching definition *) +module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs) type invariant_map diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index f73e62571..53e7eb9ef 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -8,8 +8,8 @@ open! IStd module F = Format -module D = UninitDomain.Domain (** Forward analysis to compute uninitialized variables at each program point *) +module D = UninitDomain.Domain module MaybeUninitVars = UninitDomain.MaybeUninitVars module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair) diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index e5779d5d2..027f718e9 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -50,8 +50,7 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit L.(debug Capture Verbose) "@\n Start building call/cfg graph for '%a'....@\n" SourceFile.pp source_file ; let cfg = compute_icfg translation_unit_context tenv ast in - L.(debug Capture Verbose) - "@\n End building call/cfg graph for '%a'.@\n" SourceFile.pp source_file ; + L.(debug Capture Verbose) "@\n End building call/cfg graph for '%a'.@\n" SourceFile.pp source_file ; NullabilityPreanalysis.analysis cfg tenv ; SourceFiles.add source_file cfg (Tenv.FileLocal tenv) (Some integer_type_widths) ; if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ; diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index e401bb601..b3a61788b 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -3217,8 +3217,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let field_exp = Exp.Lfield (ret_exp, field_name, typ) in let args = type_info_objc :: (field_exp, void_typ) - :: Option.value_map ~default:[] res_trans_subexpr ~f:(fun trans_result -> [trans_result.return] - ) + :: Option.value_map ~default:[] res_trans_subexpr ~f:(fun trans_result -> + [trans_result.return] ) in let call_instr = Sil.Call ((ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in let res_control = {empty_control with instrs= [call_instr]} in diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 56c039009..55befc542 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -662,8 +662,8 @@ let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks let event = Event.make_acquire lock in add_critical_pair ?tenv lock_state event astate.thread ~loc acc ) ; lock_state= - List.fold locks ~init:lock_state ~f:(fun acc lock -> LockState.acquire ~procname ~loc lock acc) - } + List.fold locks ~init:lock_state ~f:(fun acc lock -> + LockState.acquire ~procname ~loc lock acc ) } let make_call_with_event new_event ~loc astate = diff --git a/infer/src/cost/hoisting.ml b/infer/src/cost/hoisting.ml index 51c782cff..1a90cf618 100644 --- a/infer/src/cost/hoisting.ml +++ b/infer/src/cost/hoisting.ml @@ -25,8 +25,8 @@ end module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node) module HoistCalls = AbstractDomain.FiniteSet (Call) -module LoopHeadToHoistInstrs = Procdesc.NodeMap (** Map loop_header -> instrs that can be hoisted out of the loop *) +module LoopHeadToHoistInstrs = Procdesc.NodeMap (* A loop-invariant function call C(args) at node N can be hoisted out of the loop if * diff --git a/infer/src/integration/Differential.ml b/infer/src/integration/Differential.ml index 7ad684ea3..2228d89b1 100644 --- a/infer/src/integration/Differential.ml +++ b/infer/src/integration/Differential.ml @@ -124,8 +124,7 @@ module CostsSummary = struct let json_degrees = DegreeMap.bindings paired_counts.degrees |> List.map ~f:(fun (key, {current; previous}) -> - `Assoc [("degree", `Int key); ("current", `Int current); ("previous", `Int previous)] - ) + `Assoc [("degree", `Int key); ("current", `Int current); ("previous", `Int previous)] ) in let create_assoc current previous = `Assoc [("current", `Int current); ("previous", `Int previous)] diff --git a/infer/src/integration/JsonReports.ml b/infer/src/integration/JsonReports.ml index 97e8926f1..41e2894dc 100644 --- a/infer/src/integration/JsonReports.ml +++ b/infer/src/integration/JsonReports.ml @@ -321,8 +321,7 @@ let process_all_summaries_and_issues ~issues_outf ~costs_outf = !all_issues ; (* Issues that are generated and stored outside of summaries by linter and checkers *) List.iter (ResultsDirEntryName.get_issues_directories ()) ~f:(fun dir_name -> - IssueLog.load dir_name |> IssueLog.iter ~f:(write_lint_issues filters issues_outf linereader) - ) ; + IssueLog.load dir_name |> IssueLog.iter ~f:(write_lint_issues filters issues_outf linereader) ) ; () diff --git a/infer/src/java/jContext.mli b/infer/src/java/jContext.mli index 5d24f84f0..b7f635d2a 100644 --- a/infer/src/java/jContext.mli +++ b/infer/src/java/jContext.mli @@ -14,9 +14,9 @@ open Sawja_pack instruction. *) type jump_kind = Next | Jump of int | Exit -module NodeTbl : Caml.Hashtbl.S with type key = Procdesc.Node.t (** Hastable for storing nodes that correspond to if-instructions. These are used when adding the edges in the contrl flow graph. *) +module NodeTbl : Caml.Hashtbl.S with type key = Procdesc.Node.t (** data structure for saving the three structures tht contain the intermediate representation of a file: the type environment, the control graph and the control flow graph *) diff --git a/infer/src/labs/00_dummy_checker/ResourceLeaks.ml b/infer/src/labs/00_dummy_checker/ResourceLeaks.ml index 949bebcef..6faced69e 100644 --- a/infer/src/labs/00_dummy_checker/ResourceLeaks.ml +++ b/infer/src/labs/00_dummy_checker/ResourceLeaks.ml @@ -74,9 +74,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/labs/01_integer_domain/ResourceLeaks.ml b/infer/src/labs/01_integer_domain/ResourceLeaks.ml index d0932c97d..7e71fe960 100644 --- a/infer/src/labs/01_integer_domain/ResourceLeaks.ml +++ b/infer/src/labs/01_integer_domain/ResourceLeaks.ml @@ -76,9 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/labs/02_domain_join/ResourceLeaks.ml b/infer/src/labs/02_domain_join/ResourceLeaks.ml index d0932c97d..7e71fe960 100644 --- a/infer/src/labs/02_domain_join/ResourceLeaks.ml +++ b/infer/src/labs/02_domain_join/ResourceLeaks.ml @@ -76,9 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/labs/03_domain_top/ResourceLeaks.ml b/infer/src/labs/03_domain_top/ResourceLeaks.ml index d0932c97d..7e71fe960 100644 --- a/infer/src/labs/03_domain_top/ResourceLeaks.ml +++ b/infer/src/labs/03_domain_top/ResourceLeaks.ml @@ -76,9 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/labs/04_interprocedural/ResourceLeaks.ml b/infer/src/labs/04_interprocedural/ResourceLeaks.ml index 7d008533c..6e77dcbd6 100644 --- a/infer/src/labs/04_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/04_interprocedural/ResourceLeaks.ml @@ -90,9 +90,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks lab" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml index 9ef4743b2..89785ea55 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml @@ -97,9 +97,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks lab" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index cd37f2e8f..989876ce9 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -68,9 +68,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end -module CFG = ProcCfg.Normal (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to ignore them *) +module CFG = ProcCfg.Normal (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) diff --git a/infer/src/nullsafe/Initializers.ml b/infer/src/nullsafe/Initializers.ml index a4ed9efe0..beb0267c4 100644 --- a/infer/src/nullsafe/Initializers.ml +++ b/infer/src/nullsafe/Initializers.ml @@ -129,7 +129,6 @@ let final_constructor_typestates_lazy tenv curr_pname typecheck_proc = lazy (let constructors_current_class = pname_and_pdescs_with tenv curr_pname (fun (pname, _) -> - Procname.is_constructor pname && equal_class_opt (get_class pname) (get_class curr_pname) - ) + Procname.is_constructor pname && equal_class_opt (get_class pname) (get_class curr_pname) ) in final_typestates constructors_current_class tenv typecheck_proc ) diff --git a/infer/src/nullsafe/unit/AggregatedSummariesTest.ml b/infer/src/nullsafe/unit/AggregatedSummariesTest.ml index 543ae0b7a..b5f3ad886 100644 --- a/infer/src/nullsafe/unit/AggregatedSummariesTest.ml +++ b/infer/src/nullsafe/unit/AggregatedSummariesTest.ml @@ -54,8 +54,7 @@ let assert_anonymous_equal actual expected_name_to_ids case_name = actual |> IOption.if_none_eval ~f:(fun () -> assert_failure - (F.sprintf "%s: Did not find anonymous class info for %s" case_name anonymous_name) - ) + (F.sprintf "%s: Did not find anonymous class info for %s" case_name anonymous_name) ) in assert_summaries_equal actual_summaries expected_summary_ids anonymous_name case_name ) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index a9c5fa92d..b0d1a28f9 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -78,8 +78,9 @@ module PostDomain : BaseDomainSig = struct end (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *) -module PreDomain : BaseDomainSig = PostDomain + (** represents the inferred pre-condition at each program point, biabduction style *) +module PreDomain : BaseDomainSig = PostDomain (** biabduction-style pre/post state + skipped calls *) type t = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 424faa902..83c121dc7 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -41,15 +41,15 @@ module type BaseDomainSig = sig val pp : F.formatter -> t -> unit end -module PostDomain : BaseDomainSig (** The post abstract state at each program point, or current state. *) +module PostDomain : BaseDomainSig -module PreDomain : BaseDomainSig (** The inferred pre-condition at each program point, biabduction style. NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. * *) +module PreDomain : BaseDomainSig (** biabduction-style pre/post state + skipped calls *) type t = private diff --git a/infer/src/pulse/PulseDomainInterface.ml b/infer/src/pulse/PulseDomainInterface.ml index 9c6014c87..97e5dde9f 100644 --- a/infer/src/pulse/PulseDomainInterface.ml +++ b/infer/src/pulse/PulseDomainInterface.ml @@ -8,15 +8,15 @@ open! IStd module ExecutionDomain = PulseExecutionDomain -module AbductiveDomain = PulseAbductiveDomain (** if you do any mutations of the state in pulse you probably want this module *) +module AbductiveDomain = PulseAbductiveDomain module Stack = AbductiveDomain.Stack module Memory = AbductiveDomain.Memory module AddressAttributes = AbductiveDomain.AddressAttributes -module BaseDomain = PulseBaseDomain (** use only if you know what you are doing or you risk break bi-abduction *) +module BaseDomain = PulseBaseDomain module BaseStack = PulseBaseStack module BaseMemory = PulseBaseMemory diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 866bbdac0..4692db861 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -20,8 +20,7 @@ let check_addr_access location (address, history) astate = let access_trace = Trace.Immediate {location; history} in AddressAttributes.check_valid access_trace address astate |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> - (Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) - ) + (Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) ) module Closures = struct @@ -46,8 +45,7 @@ module Closures = struct let mk_capture_edges captured = List.foldi captured ~init:Memory.Edges.empty ~f:(fun id edges captured_addr_trace -> - Memory.Edges.add (HilExp.Access.FieldAccess (mk_fake_field ~id)) captured_addr_trace edges - ) + Memory.Edges.add (HilExp.Access.FieldAccess (mk_fake_field ~id)) captured_addr_trace edges ) let check_captured_addresses action lambda_addr (astate : t) = diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 59b681c3b..046ce8fa1 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -294,8 +294,8 @@ let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) let prune_bo_with_bop ~negated v_opt arith bop arith' phi = match Option.both v_opt (if negated then Binop.negate bop else Some bop) - |> Option.map ~f:(fun (v, positive_bop) -> (v, Itv.ItvPure.prune_binop positive_bop arith arith') - ) + |> Option.map ~f:(fun (v, positive_bop) -> + (v, Itv.ItvPure.prune_binop positive_bop arith arith') ) with | None -> phi diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index e834e4e26..95084d108 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -471,8 +471,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct let trace, subtree = Option.value ~default:TaintDomain.empty_node (TaintDomain.get_node access_path astate) in - TaintDomain.add_node access_path (TraceDomain.add_source source trace, subtree) astate - ) + TaintDomain.add_node access_path (TraceDomain.add_source source trace, subtree) astate ) else astate diff --git a/infer/src/unit/LRUHashtblTests.ml b/infer/src/unit/LRUHashtblTests.ml index 7c42608eb..ecf660236 100644 --- a/infer/src/unit/LRUHashtblTests.ml +++ b/infer/src/unit/LRUHashtblTests.ml @@ -54,5 +54,4 @@ let tests = "LRUHashtble" >::: List.map inputs ~f:(fun (name, input, expected) -> name - >:: fun _ -> assert_equal (input () |> LRUHash.bindings |> List.sort ~compare) expected - ) + >:: fun _ -> assert_equal (input () |> LRUHash.bindings |> List.sort ~compare) expected ) diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index c6f7cd471..9c72b01c9 100644 --- a/sledge/bin/frontend.ml +++ b/sledge/bin/frontend.ml @@ -967,7 +967,7 @@ let xlate_instr : (* operator delete(void* ptr, std::align_val_t) *) ] |[ "_ZdlPvmSt11align_val_t" (* operator delete(void* ptr, unsigned long, std::align_val_t) *) - ] + ] |["free" (* void free(void* ptr) *)] -> let ptr = xlate_value x (Llvm.operand instr 0) in emit_inst (Llair.Inst.free ~ptr ~loc) diff --git a/sledge/src/equality.ml b/sledge/src/equality.ml index 0bc39562c..f91b81ad2 100644 --- a/sledge/src/equality.ml +++ b/sledge/src/equality.ml @@ -347,8 +347,7 @@ let classes r = Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls -> match classify key with | Interpreted | Atomic -> add key data cls - | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls - ) + | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls ) let cls_of r e = let e' = Subst.apply r.rep e in @@ -1004,8 +1003,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) = Some trm | _ -> rep_ito_us ) in - Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix - ) ) + Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix ) ) |> List.min_elt ~compare:[%compare: Term.t list] with | Some extracts -> @@ -1130,8 +1128,7 @@ let wrap tmr f call = report ~name ~elapsed ~aggregate ~count ; if Float.(elapsed > !dump_threshold) then ( dump_threshold := 2. *. !dump_threshold ; - Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) ) - ) ; + Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) ) ) ; r in if not [%debug] then f () diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 1391a29ba..214b9b814 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -750,8 +750,8 @@ let rec simplify_ us rev_xss q = (starN ( {q with us= Var.Set.union q.us q.xs; xs= emp.xs; djns= []} :: List.map q.djns ~f:(fun djn -> - orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) - ) )) + orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) ) + )) in (* try to solve equations in cong for variables in xss *) let subst = Equality.solve_for_vars (us :: List.rev rev_xss) q.cong in diff --git a/sledge/src/term.mli b/sledge/src/term.mli index 9d029f1cb..b45ab11a6 100644 --- a/sledge/src/term.mli +++ b/sledge/src/term.mli @@ -16,9 +16,9 @@ type op1 = signed integer. That is, it two's-complement--decodes the low [n] bits of the infinite two's-complement encoding of [arg]. *) | Unsigned of {bits: int} - (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an - [n]-bit unsigned integer. That is, it unsigned-binary--decodes the - low [n] bits of the infinite two's-complement encoding of [arg]. *) + (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit + unsigned integer. That is, it unsigned-binary--decodes the low [n] + bits of the infinite two's-complement encoding of [arg]. *) | Convert of {src: Typ.t; dst: Typ.t} (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src] to type [dst], possibly with loss of information. The [src] and