From acb76469b5cd2c2e30c8c35a8bb80b9301e66cfe Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 2 Apr 2020 03:41:37 -0700 Subject: [PATCH] [odoc] fix all provably-dodgy docstrings Summary: Fix all the docstrings that `odoc` or `ocamlformat` is not happy about. Delete all `[@@ocamlformat "parse-docstring = false"]` pragmas as a result. Reviewed By: jberdine, ngorogiannis Differential Revision: D20798913 fbshipit-source-id: 728d9e45c --- infer/src/IR/Typ.ml | 6 +- infer/src/IR/Typ.mli | 16 +- infer/src/absint/TransferFunctions.mli | 18 +- infer/src/al/cPredicates.mli | 466 ++++++++++------------- infer/src/backend/errdesc.ml | 58 ++- infer/src/base/SqliteUtils.ml | 2 +- infer/src/base/SqliteUtils.mli | 4 +- infer/src/biabduction/Rearrange.ml | 78 ++-- infer/src/biabduction/Tabulation.ml | 61 ++- infer/src/bufferoverrun/bounds.ml | 21 +- infer/src/bufferoverrun/polynomials.ml | 57 +-- infer/src/checkers/accessPathDomains.mli | 6 +- infer/src/checkers/accessTree.mli | 26 +- infer/src/clang/cTrans.ml | 155 ++++---- infer/src/concurrency/RacerDDomain.mli | 2 +- infer/src/cost/costDomain.ml | 10 +- infer/src/cost/costDomain.mli | 8 +- infer/src/scuba/ScubaLogging.mli | 29 +- 18 files changed, 449 insertions(+), 574 deletions(-) diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 894430b92..253d8357e 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -6,8 +6,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - (** The Smallfoot Intermediate Language: Types *) open! IStd @@ -540,8 +538,8 @@ let is_ptr_to_ignore_quals t ~ptr = match ptr.desc with Tptr (t', _) -> equal_ignore_quals t t' | _ -> false -(** If an array type, return the type of the element. - If not, return the default type if given, otherwise raise an exception *) +(** If an array type, return the type of the element. If not, return the default type if given, + otherwise raise an exception *) let array_elem default_opt typ = match typ.desc with Tarray {elt} -> elt | _ -> unsome "array_elem" default_opt diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 1415663f9..90fd3e016 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -6,8 +6,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - (** The Smallfoot Intermediate Language: Types *) open! IStd @@ -121,18 +119,20 @@ and template_spec_info = | Template of { mangled: string option (** WARNING: because of type substitutions performed by [sub_type] and [sub_tname], - mangling is not guaranteed to be unique to a single type. All the information in - the template arguments is also needed for uniqueness. *) + mangling is not guaranteed to be unique to a single type. All the information in the + template arguments is also needed for uniqueness. *) ; args: template_arg list } [@@deriving compare] val pp_template_spec_info : Pp.env -> F.formatter -> template_spec_info -> unit [@@warning "-32"] val mk : ?default:t -> ?quals:type_quals -> desc -> t -(** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals *) +(** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such + as quals *) val mk_array : ?default:t -> ?quals:type_quals -> ?length:IntLit.t -> ?stride:IntLit.t -> t -> t -(** Create an array type from a given element type. If [length] or [stride] value is given, use them as static length and size. *) +(** Create an array type from a given element type. If [length] or [stride] value is given, use them + as static length and size. *) val mk_struct : name -> t @@ -302,8 +302,8 @@ val is_ptr_to_ignore_quals : t -> ptr:t -> bool (** check if [ptr] is a pointer type to [t], ignoring quals *) val array_elem : t option -> t -> t -(** If an array type, return the type of the element. - If not, return the default type if given, otherwise raise an exception *) +(** If an array type, return the type of the element. If not, return the default type if given, + otherwise raise an exception *) val is_objc_class : t -> bool diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 8e779ede5..f2a7512a6 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd (** Transfer functions that push abstract states across instructions. A typical client should @@ -25,7 +23,11 @@ module type S = sig type instr val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t - (** {A} instr {A'}. [node] is the node of the current instruction *) + (** [exec_instr astate proc_data node instr] should usually return [astate'] such that + [{astate} instr {astate'}] is a valid Hoare triple. In other words, [exec_instr] defines how + executing an instruction from a given abstract state changes that state into a new one. This + is usually called the {i transfer function} in Abstract Interpretation terms. [node] is the + node containing the current instruction. *) val pp_session_name : CFG.Node.t -> Format.formatter -> unit (** print session name for HTML debug *) @@ -43,8 +45,8 @@ module type DisjunctiveConfig = sig val join_policy : [ `UnderApproximateAfter of int (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it, - drop any further states on the floor. This corresponds to an under-approximation/bounded - approach. *) + drop any further states on the floor. This corresponds to an under-approximation/bounded + approach. *) | `NeverJoin (** keep accumaluting states *) ] val widen_policy : [`UnderApproximateAfterNumIterations of int] @@ -63,9 +65,9 @@ module type DisjReady = sig end (** 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 - disjunct independently. The join on the disjunctive state is governed by the policy described in - [DConfig]. *) + disjunction between these states. The transfer functions are executed on each state in the + disjunct independently. The join on the disjunctive state is governed by the policy described in + [DConfig]. *) module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveConfig) : sig module Disjuncts : sig type t diff --git a/infer/src/al/cPredicates.mli b/infer/src/al/cPredicates.mli index 2fba722bf..fc7dd2ba3 100644 --- a/infer/src/al/cPredicates.mli +++ b/infer/src/al/cPredicates.mli @@ -5,13 +5,10 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd -type t = ALVar.formula_id * ALVar.alexp list [@@deriving compare] - (** (name, [param1,...,paramK]) *) +type t = ALVar.formula_id * ALVar.alexp list [@@deriving compare] val captured_variables_cxx_ref : Ctl_parser_types.ast_node -> Clang_ast_t.named_decl_info list (** list of cxx references captured by an ObjC Block *) @@ -23,77 +20,85 @@ val objc_block_is_capturing_values : Ctl_parser_types.ast_node -> bool (** true if the ObjC Block captures any variables *) val call_method : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'call_method an m an' is true iff node an is a call to an ObjC method with name containing string m *) +(** [call_method an m an] is true iff node an is a call to an ObjC method with name containing + string m *) val call_cxx_method : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'call_cxx_method an m an' is true iff node an is a call to a C++ method with name containing string m *) +(** [call_cxx_method an m an] is true iff node an is a call to a C++ method with name containing + string m *) val call_class_method : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'call_class_method an mname' is true iff node an is a call to an ObjC - class method with name containing mname *) +(** [call_class_method an mname] is true iff node an is a call to an ObjC class method with name + containing mname *) val call_instance_method : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'call_instance_method an mname' is true iff node an is a call to an ObjC - instance method with name containing mname *) +(** [call_instance_method an mname] is true iff node an is a call to an ObjC instance method with + name containing mname *) val declaration_name : Clang_ast_t.decl -> string option -(** 'declaration_name d' returns the name of declaration d *) +(** [declaration_name d] returns the name of declaration d *) val is_enum_constant : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'is_enum_constant an name' is true iff an is an EnumConstant with name containing 'name' *) +(** [is_enum_constant an name] is true iff an is an EnumConstant with name containing [name] *) val is_enum_constant_of_enum : Ctl_parser_types.ast_node -> ALVar.alexp -> bool val is_global_var : Ctl_parser_types.ast_node -> bool -(** 'is_global_var an' is true iff an is a global variable (but not a static local) *) +(** [is_global_var an] is true iff an is a global variable (but not a static local) *) val is_static_local_var : Ctl_parser_types.ast_node -> bool -(** 'is_static_local_var an' is true iff an is a static local variable *) +(** [is_static_local_var an] is true iff an is a static local variable *) val is_static_var : Ctl_parser_types.ast_node -> bool -(** 'is_static_var an' is true iff an is a static local variable *) +(** [is_static_var an] is true iff an is a static local variable *) val is_extern_var : Ctl_parser_types.ast_node -> bool -(** 'is_extern_var an' is true iff an is a extern variable *) +(** [is_extern_var an] is true iff an is a extern variable *) val is_const_expr_var : Ctl_parser_types.ast_node -> bool -(** 'is_const_expr_var an' is true iff an is a 'const' variable declaration *) +(** [is_const_expr_var an] is true iff an is a [const] variable declaration *) val is_init_integral_constant_expr : Ctl_parser_types.ast_node -> bool -(** 'is_init_integra_constant_expr an' is true iff it is an initializer and an integral constant expression, or in C++11, whether the initializer is a constant expression. *) +(** [is_init_integra_constant_expr an] is true iff it is an initializer and an integral constant + expression, or in C++11, whether the initializer is a constant expression. *) val is_qual_type_const : Ctl_parser_types.ast_node -> bool -(** 'is_qual_type_const an' is true iff an is a qual_type 'const' expression *) +(** [is_qual_type_const an] is true iff an is a qual_type [const] expression *) val has_init_list_const_expr : Ctl_parser_types.ast_node -> bool -(** 'has_init_list_const_expr' is true iff for an InitListExpr where all subexpressions are const expression *) +(** [has_init_list_const_expr] is true iff for an InitListExpr where all subexpressions are const + expression *) val call_function : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'call_function an name' is true iff an is a call to a function whose name contains 'name' *) +(** [call_function an name] is true iff an is a call to a function whose name contains [name] *) val call_qualified_function : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'call_function an name' is true iff an is a call to a function whose fully qualified name contains 'name' *) +(** [call_function an name] is true iff an is a call to a function whose fully qualified name + contains [name] *) val is_strong_property : Ctl_parser_types.ast_node -> bool -(** 'is_strong_property an' is true iff an denotes a objc property declaration with 'strong' attribute *) +(** [is_strong_property an] is true iff an denotes a objc property declaration with [strong] + attribute *) val is_strong_ivar : Ctl_parser_types.ast_node -> bool -(** 'is_strong_ivar an' is true iff an denotes a objc ivar with 'strong' attribute *) +(** [is_strong_ivar an] is true iff an denotes a objc ivar with [strong] attribute *) val is_weak_property : Ctl_parser_types.ast_node -> bool -(** 'is_weak_property an' is true iff an denotes a objc property declaration with 'weak' attribute *) +(** [is_weak_property an] is true iff an denotes a objc property declaration with [weak] attribute *) val is_assign_property : Ctl_parser_types.ast_node -> bool -(** 'is_assign_property an' is true iff an denotes a objc property declaration with 'assign' attribute *) +(** [is_assign_property an] is true iff an denotes a objc property declaration with [assign] + attribute *) val is_property_pointer_type : Ctl_parser_types.ast_node -> bool -(** 'is_property_pointer_type an' is true iff an denotes a objc property declaration with type pointer *) +(** [is_property_pointer_type an] is true iff an denotes a objc property declaration with type + pointer *) val context_in_synchronized_block : CLintersContext.context -> bool (** true if the current node is in the context of a synchronized objc block *) val is_ivar_atomic : Ctl_parser_types.ast_node -> bool -(** 'is_ivar_atomic an' is true iff an denotes an atomi objc ivar *) +(** [is_ivar_atomic an] is true iff an denotes an atomi objc ivar *) val is_method_property_accessor_of_ivar : Ctl_parser_types.ast_node -> CLintersContext.context -> bool @@ -102,317 +107,253 @@ val is_in_block : CLintersContext.context -> bool (** true if the current node is in the context of an objc block *) val is_optional_objc_method : Ctl_parser_types.ast_node -> bool -(** true if the current node is an objc method declaration which is declared with @optional *) +(** true if the current node is an objc method declaration which is declared with [@optional] *) val is_call_to_optional_objc_method : Ctl_parser_types.ast_node -> bool -(** true if the current node is a call to an objc method declaration which is declared with @optional *) +(** true if the current node is a call to an objc method declaration which is declared with + [@optional] *) val is_in_cxx_constructor : CLintersContext.context -> ALVar.alexp -> bool -(** 'is_in_cxx_constructor context name' is true if the curent node is within a CXX constructor whose name contains 'name' *) +(** [is_in_cxx_constructor context name] is true if the curent node is within a CXX constructor + whose name contains [name] *) val is_in_cxx_destructor : CLintersContext.context -> ALVar.alexp -> bool -(** 'is_in_destructor_constructor context name' is true if the curent node is within a CXX destructor whose name contains 'name' *) +(** [is_in_destructor_constructor context name] is true if the curent node is within a CXX + destructor whose name contains [name] *) val is_in_cxx_method : CLintersContext.context -> ALVar.alexp -> bool -(** 'is_in_cxx_method context name' is true if the curent node is within a CXX method whose name contains 'name' *) +(** [is_in_cxx_method context name] is true if the curent node is within a CXX method whose name + contains [name] *) val is_in_function : CLintersContext.context -> ALVar.alexp -> bool -(** 'is_in_function context name' is true if the curent node is within a function whose name contains 'name' *) +(** [is_in_function context name] is true if the curent node is within a function whose name + contains [name] *) val is_objc_extension : CLintersContext.context -> bool -(** - * Checks if the current file has an ObjC file extension (I.E. '.m' or '.mm') - *) +(** Checks if the current file has an ObjC file extension (I.E. [.m] or [.mm]) *) val is_objc_class_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCInterfaceDecl or ObjCImplementationDecl - * node whose name matches the provided REGEXP - * - * Matches on MyClass in: - * @interface MyClass - * @implementation MyClass - *) +(** Checks if the current node is an ObjCInterfaceDecl or ObjCImplementationDecl node whose name + matches the provided REGEXP + + Matches on [MyClass] in: + + {[ + @interface MyClass + @implementation MyClass + ]} *) val is_objc_interface_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCInterfaceDecl node - * whose name matches the provided REGEXP - * - * Matches on MyClass in @interface MyClass - *) +(** Checks if the current node is an ObjCInterfaceDecl node whose name matches the provided REGEXP + + Matches on [MyClass] in [@interface MyClass] *) val is_objc_implementation_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCImplementationDecl node - * whose name matches the provided REGEXP - * - * Matches on MyClass in @implementation MyClass - *) +(** Checks if the current node is an ObjCImplementationDecl node whose name matches the provided + REGEXP + + Matches on [MyClass] in [@implementation MyClass] *) val is_objc_category_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryDecl or ObjCCategoryImplDecl - * node whose name matches the provided REGEXP - * - * Matches on MyCategory in: - * @interface MyClass (MyCategory) - * @implementation MyClass (MyCategory) - *) +(** Checks if the current node is an ObjCCategoryDecl or ObjCCategoryImplDecl node whose name + matches the provided REGEXP + + Matches on [MyCategory] in: + + {[ + @interface MyClass (MyCategory) + @implementation MyClass (MyCategory) + ]} *) val is_objc_category_interface_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryDecl node - * whose name matches the provided REGEXP - * - * Matches on MyCategory in @interface MyClass (MyCategory) - *) +(** Checks if the current node is an ObjCCategoryDecl node whose name matches the provided REGEXP + + Matches on [MyCategory] in [@interface MyClass (MyCategory)] *) val is_objc_category_implementation_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryImplDecl node - * whose name matches the provided REGEXP - * - * Matches on MyCategory in @implementation MyClass (MyCategory) - *) +(** Checks if the current node is an ObjCCategoryImplDecl node whose name matches the provided + REGEXP + + Matches on [MyCategory] in [@implementation MyClass (MyCategory)] *) val is_objc_category_on_class_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryDecl or ObjCCategoryImplDecl - * node whose class's name matches the provided REGEXP - * - * Matches on MyClass in: - * @interface MyClass (MyCategory) - * @implementation MyClass (MyCategory) - *) +(** Checks if the current node is an ObjCCategoryDecl or ObjCCategoryImplDecl node whose class name + matches the provided REGEXP + + Matches on [MyClass] in: + + {[ + @interface MyClass (MyCategory) + @implementation MyClass (MyCategory) + ]} *) val is_objc_category_interface_on_class_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryDecl node - * whose class's name matches the provided REGEXP - * - * Matches on MyClass in @interface MyClass (MyCategory) - *) +(** Checks if the current node is an ObjCCategoryDecl node whose class name matches the provided + REGEXP + + Matches on [MyClass] in [@interface MyClass (MyCategory)] *) val is_objc_category_implementation_on_class_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryImplDecl node - * whose class's name matches the provided REGEXP - * - * Matches on MyClass in @implementation MyClass (MyCategory) - *) +(** Checks if the current node is an ObjCCategoryImplDecl node whose class name matches the provided + REGEXP + + Matches on [MyClass] in [@implementation MyClass (MyCategory)] *) val is_objc_category_on_subclass_of : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryDecl or ObjCCategoryImplDecl - * node whose class inherits from a class whose name matches the provided REGEXP - *) +(** Checks if the current node is an ObjCCategoryDecl or ObjCCategoryImplDecl node whose class + inherits from a class whose name matches the provided REGEXP *) val is_objc_category_interface_on_subclass_of : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryDecl node whose class - * inherits from a class whose name matches the provided REGEXP - *) +(** Checks if the current node is an ObjCCategoryDecl node whose class inherits from a class whose + name matches the provided REGEXP *) val is_objc_category_implementation_on_subclass_of : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCCategoryImplDecl node whose class - * inherits from a class whose name matches the provided REGEXP - *) +(** Checks if the current node is an ObjCCategoryImplDecl node whose class inherits from a class + whose name matches the provided REGEXP *) val adhere_to_protocol : Ctl_parser_types.ast_node -> bool -(** true if an objC class adhere to a protocol *) +(** true if an objC class adhere to a protocol *) val is_objc_protocol_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCProtocolDecl node - * whose name matches the provided REGEXP - *) +(** Checks if the current node is an ObjCProtocolDecl node whose name matches the provided REGEXP *) val is_objc_class_method_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCMethodDecl node whose name - * matches the provided REGEXP and is a class method - *) +(** Checks if the current node is an ObjCMethodDecl node whose name matches the provided REGEXP and + is a class method *) val is_objc_instance_method_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCMethodDecl node whose name - * matches the provided REGEXP and is an instance method - *) +(** Checks if the current node is an ObjCMethodDecl node whose name matches the provided REGEXP and + is an instance method *) val is_objc_method_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCMethodDecl node - * whose name matches the provided REGEXP - *) +(** Checks if the current node is an ObjCMethodDecl node whose name matches the provided REGEXP *) val is_objc_constructor : CLintersContext.context -> bool -(** 'is_in_objc_constructor context' is true if the curent node is within an ObjC constructor *) +(** [is_in_objc_constructor context] is true if the curent node is within an ObjC constructor *) val objc_class_has_only_one_constructor_method_named : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** true if an ObjC class has only one class method and is a constructor -whose name matches the provided REGEXP *) +(** true if an ObjC class has only one class method and is a constructor whose name matches the + provided REGEXP *) val is_objc_dealloc : CLintersContext.context -> bool -(** 'is_in_objc_dealloc context' is true if the curent node is within an ObjC dealloc method *) +(** [is_in_objc_dealloc context] is true if the curent node is within an ObjC dealloc method *) val is_in_objc_subclass_of : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCInterfaceDecl or - * ObjCImplementationDecl node which inherits from a class whose - * name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCInterfaceDecl or ObjCImplementationDecl node + which inherits from a class whose name matches the provided REGEXP *) val is_in_objc_interface_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCInterfaceDecl - * node whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCInterfaceDecl node whose name matches the + provided REGEXP *) val is_in_objc_implementation_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCImplementationDecl - * node whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCImplementationDecl node whose name matches the + provided REGEXP *) val is_in_objc_class_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCInterfaceDecl or - * ObjCImplementationDecl node whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCInterfaceDecl or ObjCImplementationDecl node + whose name matches the provided REGEXP *) val is_in_objc_category_interface_on_class_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryDecl node - * whose class's name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryDecl node whose class name matches the + provided REGEXP *) val is_in_objc_category_implementation_on_class_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryImplDecl node - * whose class's name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryImplDecl node whose class name matches + the provided REGEXP *) val is_in_objc_category_on_class_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryDecl or - * ObjCCategoryImplDecl node whose class's name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryDecl or ObjCCategoryImplDecl node + whose class name matches the provided REGEXP *) val is_in_objc_category_interface_on_subclass_of : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryDecl node - * whose class inherits from a class whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryDecl node whose class inherits from a + class whose name matches the provided REGEXP *) val is_in_objc_category_implementation_on_subclass_of : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryImplDecl node - * whose class inherits from a class whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryImplDecl node whose class inherits + from a class whose name matches the provided REGEXP *) val is_in_objc_category_on_subclass_of : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryDecl or - * ObjCCategoryImplDecl node whose class inherits from a class whose - * name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryDecl or ObjCCategoryImplDecl node + whose class inherits from a class whose name matches the provided REGEXP *) val is_in_objc_category_interface_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryDecl node - * whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryDecl node whose name matches the + provided REGEXP *) val is_in_objc_category_implementation_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryImplDecl node - * whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryImplDecl node whose name matches the + provided REGEXP *) val is_in_objc_category_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCCategoryDecl or - * ObjCCategoryImplDecl node whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCCategoryDecl or ObjCCategoryImplDecl node + whose name matches the provided REGEXP *) val is_in_objc_protocol_named : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node is a subnode of an ObjCProtocolDecl - * node whose name matches the provided REGEXP - *) +(** Checks if the current node is a subnode of an ObjCProtocolDecl node whose name matches the + provided REGEXP *) val is_in_objc_class_method : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node, or a parent node, is an ObjCMethodDecl node - * whose name matches the provided REGEXP and is a class method - *) +(** Checks if the current node, or a parent node, is an ObjCMethodDecl node whose name matches the + provided REGEXP and is a class method *) val is_in_objc_instance_method : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node, or a parent node, is an ObjCMethodDecl node - * whose name matches the provided REGEXP and is an instance method - *) +(** Checks if the current node, or a parent node, is an ObjCMethodDecl node whose name matches the + provided REGEXP and is an instance method *) val is_in_objc_method : CLintersContext.context -> ALVar.alexp -> bool -(** - * Checks if the current node, or a parent node, is an ObjCMethodDecl node - * whose name matches the provided REGEXP - *) +(** Checks if the current node, or a parent node, is an ObjCMethodDecl node whose name matches the + provided REGEXP *) val is_objc_method_overriding : Ctl_parser_types.ast_node -> bool -(** - * Checks if the current node is an ObjCMethodDecl node and is overriding a - * method in the superclass. - * - * A method is said to override any method in the class's base classes, - * its protocols, or its categories' protocols, that has the same selector - * and is of the same kind (class or instance). A method in an implementation - * is not considered as overriding the same method in the interface or its categories. - *) +(** Checks if the current node is an ObjCMethodDecl node and is overriding a method in the + superclass. + + A method is said to override any method in the class base classes, its protocols, or its + categories' protocols, that has the same selector and is of the same kind (class or instance). A + method in an implementation is not considered as overriding the same method in the interface or + its categories. *) val is_objc_method_exposed : CLintersContext.context -> Ctl_parser_types.ast_node -> bool -(** - * Checks if the current node is an ObjCMethodDecl node and is exposed in an interface. - * - * A method is said to be exposed if it's overriding a method or it's declared - * in a matching interface. For example, a method defined in a class's - * implementation is exposed if it's declared in the class's interface or - * interface extension, but not if it's declared in a category on the class. - * If the current node is a subnode of an ObjCInterfaceDecl, ObjCCategoryDecl, - * or ObjCProtocolDecl, this predicate returns false. - *) +(** Checks if the current node is an ObjCMethodDecl node and is exposed in an interface. + + A method is said to be exposed if it's overriding a method or it's declared in a matching + interface. For example, a method defined in a class implementation is exposed if it's declared + in the class interface or interface extension, but not if it's declared in a category on the + class. If the current node is a subnode of an ObjCInterfaceDecl, ObjCCategoryDecl, or + ObjCProtocolDecl, this predicate returns false. *) val captures_cxx_references : Ctl_parser_types.ast_node -> bool -(** 'captures_cxx_references an' is true iff the node an captures some CXX references *) +(** [captures_cxx_references an] is true iff the node an captures some CXX references *) val is_binop_with_kind : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'is_binop_with_kind an binop' is true iff an denotes a binary operator of kind binop *) +(** [is_binop_with_kind an binop] is true iff an denotes a binary operator of kind binop *) val is_unop_with_kind : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'is_unop_of_kind an unop' is true iff an denotes a unary operator of kind unop *) +(** [is_unop_of_kind an unop] is true iff an denotes a unary operator of kind unop *) val has_cast_kind : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'has_cast_kind an cast' is true iff an denotes a cast operation of kind cast *) +(** [has_cast_kind an cast] is true iff an denotes a cast operation of kind cast *) val isa : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** node an is of class classname *) +(** node an is of class classname *) val is_node : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'is_node an nodename' is true iff an is a node of kind nodename *) +(** [is_node an nodename] is true iff an is a node of kind nodename *) val declaration_has_name : Ctl_parser_types.ast_node -> ALVar.alexp -> bool val declaration_ref_name : ?kind:Clang_ast_t.decl_kind -> Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** 'declaration_ref_has_name an n' is true iff node an is a DeclRefExpr with name containing string n. The optional parameter kind -allow to distinguish between special kind of decl_ref_exprs like 'is_enum_constant'. *) +(** [declaration_ref_has_name an n] is true iff node an is a DeclRefExpr with name containing string + n. The optional parameter kind allow to distinguish between special kind of decl_ref_exprs like + [is_enum_constant]. *) val is_class : Ctl_parser_types.ast_node -> ALVar.alexp -> bool @@ -449,47 +390,35 @@ val receiver_class_method_call : Ctl_parser_types.ast_node -> Clang_ast_t.decl o val receiver_method_call : Ctl_parser_types.ast_node -> Clang_ast_t.decl option val is_receiver_objc_class_type : Ctl_parser_types.ast_node -> bool -(** - * Checks if the current node is an ObjCMessageExpr node and has a - * receiver equivalent to the 'Class' type. - *) +(** Checks if the current node is an ObjCMessageExpr node and has a receiver equivalent to the + [Class] type. *) val is_receiver_objc_id_type : Ctl_parser_types.ast_node -> bool -(** - * Checks if the current node is an ObjCMessageExpr node and has a - * receiver equivalent to the 'id' type. - *) +(** Checks if the current node is an ObjCMessageExpr node and has a receiver equivalent to the [id] + type. *) val is_receiver_subclass_of : CLintersContext.context -> Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCMessageExpr node and has a receiver - * which inherits from a class whose name matches the provided REGEXP. - *) +(** Checks if the current node is an ObjCMessageExpr node and has a receiver which inherits from a + class whose name matches the provided REGEXP. *) val is_receiver_class_named : CLintersContext.context -> Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * Checks if the current node is an ObjCMessageExpr node and has a - * receiver whose class name matches the provided REGEXP. - *) +(** Checks if the current node is an ObjCMessageExpr node and has a receiver whose class name + matches the provided REGEXP. *) val is_receiver_super : Ctl_parser_types.ast_node -> bool -(** - * Checks if the current node is an ObjCMessageExpr node and has a - * receiver which is equal to 'super'. - * - * Matches on [super myMethod]; - *) +(** Checks if the current node is an ObjCMessageExpr node and has a receiver which is equal to + [super]. + + Matches on [super myMethod]; *) val is_receiver_self : Ctl_parser_types.ast_node -> bool -(** - * Checks if the current node is an ObjCMessageExpr node and has a - * receiver which is equal to 'self'. - *) +(** Checks if the current node is an ObjCMessageExpr node and has a receiver which is equal to + [self]. *) val is_at_selector_with_name : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** an is an expression @selector with whose name in the language of re *) +(** an is an expression [@selector] with whose name in the language of re *) val has_visibility_attribute : Ctl_parser_types.ast_node -> ALVar.alexp -> bool @@ -519,34 +448,27 @@ val is_cxx_copy_constructor : Ctl_parser_types.ast_node -> bool (** true if the current node is a C++ copy constructor *) val has_cxx_fully_qualified_name : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** true iff node has C++ fully qualified name (w/class and namespace) - * matching the given regexp - *) +(** true iff node has C++ fully qualified name (w/class and namespace) matching the given regexp *) val has_cxx_fully_qualified_name_in_custom_symbols : Ctl_parser_types.ast_node -> string -> bool -(** true iff node has C++ fully qualified name (w/class and namespace) - * matching a prefix on the given named custom symbol list - *) +(** true iff node has C++ fully qualified name (w/class and namespace) matching a prefix on the + given named custom symbol list *) val is_in_source_file : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * True iff the source file path of the given node matches the given regexp or string. - *) +(** True iff the source file path of the given node matches the given regexp or string. *) val is_referencing_decl_from_source_file : Ctl_parser_types.ast_node -> ALVar.alexp -> bool -(** - * True iff the given node is a DeclRefExpr referencing a decl whose source file path matches the given regexp or string. - *) +(** True iff the given node is a DeclRefExpr referencing a decl whose source file path matches the + given regexp or string. *) val is_cxx_method_overriding : Ctl_parser_types.ast_node -> ALVar.alexp option -> bool -(** - * True iff the current node is a CXXMethodDecl node and is overriding a - * method whose fully-qualified name (with class and namespace) matches - * the given regexp (if given, otherwise any overriding method satisfies). - *) +(** True iff the current node is a CXXMethodDecl node and is overriding a method whose + fully-qualified name (with class and namespace) matches the given regexp (if given, otherwise + any overriding method satisfies). *) val is_init_expr_cxx11_constant : Ctl_parser_types.ast_node -> bool -(** true if the current node is classified as C++11 constant expression by the AST. It works only for VarDecl init expr *) +(** true if the current node is classified as C++11 constant expression by the AST. It works only + for VarDecl init expr *) val cxx_construct_expr_has_no_parameters : Ctl_parser_types.ast_node -> bool (** true if a construct expr has no subexpressions *) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 7d458a696..cfecb5324 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -6,8 +6,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd (** Create descriptions of analysis errors *) @@ -74,8 +72,8 @@ let explain_deallocate_constant_string s ra = let verbose = Config.trace_error -(** Find the function call instruction used to initialize normal variable [id], - and return the function name and arguments *) +(** Find the function call instruction used to initialize normal variable [id], and return the + function name and arguments *) let find_normal_variable_funcall (node : Procdesc.Node.t) (id : Ident.t) : (Exp.t * Exp.t list * Location.t * CallFlags.t) option = let find_declaration _ = function @@ -103,10 +101,9 @@ let find_program_variable_assignment node pvar : (Procdesc.Node.t * Ident.t) opt Procdesc.Node.find_in_node_or_preds node ~f:find_instr -(** Special case for C++, where we translate code like - `struct X; X getX() { X x; return X; }` as - `void getX(struct X * frontend_generated_pvar)`. - This lets us recognize that X was returned from getX *) +(** Special case for C++, where we translate code like [struct X; X getX() { X x; return X; }] as + [void getX(struct X * frontend_generated_pvar)]. This lets us recognize that X was returned from + getX *) let find_struct_by_value_assignment node pvar = if Pvar.is_frontend_tmp pvar then let find_instr node = function @@ -134,8 +131,8 @@ let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option = Procdesc.Node.find_in_node_or_preds node ~f:find_instr -(** Find a boolean assignment to a temporary variable holding a boolean condition. - The boolean parameter indicates whether the true or false branch is required. *) +(** Find a boolean assignment to a temporary variable holding a boolean condition. The boolean + parameter indicates whether the true or false branch is required. *) let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = let find_instr n = let filter = function @@ -155,8 +152,8 @@ let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = None -(** Find the Load instruction used to declare normal variable [id], - and return the expression dereferenced to initialize [id] *) +(** Find the Load instruction used to declare normal variable [id], and return the expression + dereferenced to initialize [id] *) let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t option = let find_declaration node = function | Sil.Load {id= id0; e} when Ident.equal id id0 -> @@ -381,8 +378,7 @@ let exp_lv_dexp tenv = exp_lv_dexp_ tenv Exp.Set.empty let exp_rv_dexp tenv = exp_rv_dexp_ tenv Exp.Set.empty -(** Produce a description of a mismatch between an allocation function - and a deallocation function *) +(** Produce a description of a mismatch between an allocation function and a deallocation function *) let explain_allocation_mismatch ra_alloc ra_dealloc = let get_primitive_called is_alloc ra = (* primitive alloc/dealloc function ultimately used, and function actually called *) @@ -402,8 +398,8 @@ let explain_allocation_mismatch ra_alloc ra_dealloc = (get_primitive_called false ra_dealloc) -(** check whether the type of leaked [hpred] appears as a predicate - in an inductive predicate in [prop] *) +(** check whether the type of leaked [hpred] appears as a predicate in an inductive predicate in + [prop] *) let leak_from_list_abstraction hpred prop = let hpred_type (hpred : Predicates.hpred) = match hpred with @@ -453,10 +449,9 @@ let find_typ_without_ptr prop pvar = !res -(** Produce a description of a leak by looking at the current state. - If the current instruction is a variable nullify, blame the variable. - If it is an abstraction, blame any variable nullify at the current node. - If there is an alloc attribute, print the function call and line number. *) +(** Produce a description of a leak by looking at the current state. If the current instruction is a + variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the + current node. If there is an alloc attribute, print the function call and line number. *) let explain_leak tenv hpred prop alloc_att_opt bucket = let instro = State.get_instr () in let loc = State.get_loc_exn () in @@ -565,8 +560,8 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (exn_cat, Localise.desc_leak hpred_typ_opt value_str resource_opt res_action_opt loc bucket) -(** find the dexp, if any, where the given value is stored - also return the type of the value if found *) +(** find the dexp, if any, where the given value is stored also return the type of the value if + found *) let vpath_find tenv prop exp_ : DExp.t option * Typ.t option = if verbose then (L.d_str "in vpath_find exp:" ; Exp.d_exp exp_ ; L.d_ln ()) ; let rec find sigma_acc sigma_todo exp = @@ -942,10 +937,9 @@ let rec find_outermost_dereference tenv node e = None -(** explain memory access performed by the current instruction - if outermost_array is true, the outermost array access is removed - if outermost_dereference is true, stop at the outermost dereference - (skipping e.g. outermost field access) *) +(** explain memory access performed by the current instruction if outermost_array is true, the + outermost array access is removed if outermost_dereference is true, stop at the outermost + dereference (skipping e.g. outermost field access) *) let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = false) ?(outermost_dereference = false) ?(is_nullable = false) ?(is_premature_nil = false) deref_str prop loc = @@ -1003,8 +997,8 @@ let explain_dereference proc_name tenv ?(use_buckets = false) ?(is_nullable = fa ~is_nullable ~is_premature_nil deref_str prop loc -(** Produce a description of the array access performed in the current instruction, if any. - The subexpression to focus on is obtained by removing the outermost array access. *) +(** Produce a description of the array access performed in the current instruction, if any. The + subexpression to focus on is obtained by removing the outermost array access. *) let explain_array_access tenv deref_str prop loc = explain_access_ tenv ~outermost_array:true deref_str prop loc @@ -1029,8 +1023,8 @@ let dexp_apply_pvar_off dexp pvar_off = (* case should not happen *) -(** Produce a description of the nth parameter of the function call, if the current instruction - is a function call with that parameter *) +(** Produce a description of the nth parameter of the function call, if the current instruction is a + function call with that parameter *) let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n pvar_off = let node = State.get_node_exn () in let loc = State.get_loc_exn () in @@ -1083,8 +1077,8 @@ let find_with_exp prop exp = !res -(** return a description explaining value [exp] in [prop] in terms of a source expression - using the formal parameters of the call *) +(** return a description explaining value [exp] in [prop] in terms of a source expression using the + formal parameters of the call *) let explain_dereference_as_caller_expression proc_name tenv ?(use_buckets = false) deref_str actual_pre spec_pre exp node loc formal_params = let find_formal_param_number name = diff --git a/infer/src/base/SqliteUtils.ml b/infer/src/base/SqliteUtils.ml index 38aabbe13..376cffc1a 100644 --- a/infer/src/base/SqliteUtils.ml +++ b/infer/src/base/SqliteUtils.ml @@ -20,7 +20,7 @@ let check_result_code db ~log rc = let exec db ~log ~stmt = - (* Call [check_result_code] with [fatal:true] and catch exceptions to rewrite the error message. This avoids allocating the error string when not needed. *) + (* Call [check_result_code] and catch exceptions to rewrite the error message. This avoids allocating the error string when not needed. *) PerfEvent.log (fun logger -> PerfEvent.log_begin_event logger ~name:"sql exec" ~arguments:[("stmt", `String log)] () ) ; let rc = Sqlite3.exec db stmt in diff --git a/infer/src/base/SqliteUtils.mli b/infer/src/base/SqliteUtils.mli index 1f6089ce1..375e21f3d 100644 --- a/infer/src/base/SqliteUtils.mli +++ b/infer/src/base/SqliteUtils.mli @@ -13,10 +13,10 @@ 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 - valid, then if [fatal] is set raise {!Error}, otherwise log the error and proceed. *) + valid, raise {!Error}. *) val exec : Sqlite3.db -> log:string -> stmt:string -> unit -(** Execute the given Sqlite [stmt] and check the result with {!check_result_code ~fatal:true}. *) +(** Execute the given Sqlite [stmt] and check the result with {!check_result_code}. *) val finalize : Sqlite3.db -> log:string -> Sqlite3.stmt -> unit (** Finalize the given [stmt]. Raises {!Error} on failure. *) diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 1ce79d0b5..3e25befc2 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -6,8 +6,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd (** Re-arrangement and extension of structures with fresh variables *) @@ -24,11 +22,9 @@ let rec list_rev_and_concat l1 l2 = match l1 with [] -> l2 | x1 :: l1' -> list_rev_and_concat l1' (x1 :: l2) -(** Check whether the index is out of bounds. - If the length is - 1, no check is performed. - If the index is provably out of bound, a bound error is given. - If the length is a constant and the index is not provably in bound, a warning is given. -*) +(** Check whether the index is out of bounds. If the length is - 1, no check is performed. If the + index is provably out of bound, a bound error is given. If the length is a constant and the + index is not provably in bound, a warning is given. *) let check_bad_index tenv pname p len index loc = let len_is_constant = match len with Exp.Const _ -> true | _ -> false in let index_provably_out_of_bound () = @@ -183,11 +179,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp res -(** Extend the strexp by populating the path indicated by [off]. - This means that it will add missing flds and do the case - analysis - for array accesses. This does not catch the array - bounds errors. - If we want to implement the checks for array bounds errors, - we need to change this function. *) +(** Extend the strexp by populating the path indicated by [off]. This means that it will add missing + flds and do the case - analysis for array accesses. This does not catch the array - bounds + errors. If we want to implement the checks for array bounds errors, we need to change this + function. *) let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se (typ : Typ.t) (off : Predicates.offset list) inst = let new_id () = incr max_stamp ; Ident.create kind !max_stamp in @@ -443,7 +438,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst : if not (exp_has_only_footprint_ids root) then if (* in angelic mode, purposely ignore dangling pointer warnings during the footprint phase -- we - * will fix them during the re - execution phase *) + will fix them during the re-execution phase *) not !BiabductionConfig.footprint then ( L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ; @@ -489,8 +484,8 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst : (ptsto, ptsto_foot, atoms @ atoms') -(** Check if the path in exp exists already in the current ptsto predicate. - If it exists, return None. Otherwise, return [Some fld] with [fld] the missing field. *) +(** Check if the path in exp exists already in the current ptsto predicate. If it exists, return + None. Otherwise, return [Some fld] with [fld] the missing field. *) let prop_iter_check_fields_ptsto_shallow tenv iter lexp = let offset = Predicates.exp_get_offsets lexp in let _, se, _ = @@ -519,10 +514,9 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp = check_offset se offset -(** [prop_iter_extend_ptsto iter lexp] extends the current psto - predicate in [iter] with enough fields to follow the path in - [lexp] -- field splitting model. It also materializes all - indices accessed in lexp. *) +(** [prop_iter_extend_ptsto iter lexp] extends the current psto predicate in [iter] with enough + fields to follow the path in [lexp] -- field splitting model. It also materializes all indices + accessed in lexp. *) let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = if Config.trace_rearrange then ( L.d_str "entering prop_iter_extend_ptsto lexp: " ; @@ -668,11 +662,10 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = assert false -(** Add a pointsto for [root(lexp): typ] to the sigma and footprint of a - prop, if it's compatible with the allowed footprint - variables. Then, change it into a iterator. This function ensures - that [root(lexp): typ] is the current hpred of the iterator. typ - is the type of the root of lexp. *) +(** Add a pointsto for [root(lexp): typ] to the sigma and footprint of a prop, if it's compatible + with the allowed footprint variables. Then, change it into a iterator. This function ensures + that [root(lexp): typ] is the current hpred of the iterator. typ is the type of the root of + lexp. *) let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = let max_stamp = Prop.max_stamp ~f:Ident.is_footprint prop in let ptsto, ptsto_foot, atoms = @@ -701,9 +694,8 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = Prop.prop_iter_set_state iter offsets_default -(** Add a pointsto for [root(lexp): typ] to the iterator and to the - footprint, if it's compatible with the allowed footprint - variables. This function ensures that [root(lexp): typ] is the +(** Add a pointsto for [root(lexp): typ] to the iterator and to the footprint, if it's compatible + with the allowed footprint variables. This function ensures that [root(lexp): typ] is the current hpred of the iterator. typ is the type of the root of lexp. *) let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst = if Config.trace_rearrange then ( @@ -902,7 +894,8 @@ let iter_rearrange_pe_lseg tenv recurse_on_iters default_case_iter iter para e1 recurse_on_iters iter_subcases -(** do re-arrangment for an iter whose current element is a possibly empty dllseg to be unrolled from lhs *) +(** do re-arrangment for an iter whose current element is a possibly empty dllseg to be unrolled + from lhs *) let iter_rearrange_pe_dllseg_first tenv recurse_on_iters default_case_iter iter para_dll e1 e2 e3 e4 elist = let iter_inductive_case = @@ -925,7 +918,8 @@ let iter_rearrange_pe_dllseg_first tenv recurse_on_iters default_case_iter iter recurse_on_iters iter_subcases -(** do re-arrangment for an iter whose current element is a possibly empty dllseg to be unrolled from rhs *) +(** do re-arrangment for an iter whose current element is a possibly empty dllseg to be unrolled + from rhs *) let iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter para_dll e1 e2 e3 e4 elist = let iter_inductive_case = @@ -972,8 +966,8 @@ let type_at_offset tenv texp off = match texp with Exp.Sizeof {typ} -> strip_offset off typ | _ -> None -(** Check that the size of a type coming from an instruction does not exceed the size of the type from the pointsto predicate - For example, that a pointer to int is not used to assign to a char *) +(** Check that the size of a type coming from an instruction does not exceed the size of the type + from the pointsto predicate For example, that a pointer to int is not used to assign to a char *) let check_type_size tenv pname prop texp off typ_from_instr = L.d_strln ~color:Orange "check_type_size" ; L.d_str "off: " ; @@ -1002,15 +996,13 @@ let check_type_size tenv pname prop texp off typ_from_instr = L.d_str "texp: " ; Exp.d_texp_full texp ; L.d_ln () -(** Exposes lexp |->- from iter. In case that it is not possible to - * expose lexp |->-, this function prints an error message and - * faults. There are four things to note. First, typ is the type of the - * root of lexp. Second, prop should mean the same as iter. Third, the - * result [] means that the given input iter is inconsistent. This - * happens when the theorem prover can prove the inconsistency of prop, - * only after unrolling some predicates in prop. This function ensures - * that the theorem prover cannot prove the inconsistency of any of the - * new iters in the result. *) +(** Exposes lexp |->- from iter. In case that it is not possible to * expose lexp |->-, this + function prints an error message and * faults. There are four things to note. First, typ is the + type of the * root of lexp. Second, prop should mean the same as iter. Third, the * result [] + means that the given input iter is inconsistent. This * happens when the theorem prover can + prove the inconsistency of prop, * only after unrolling some predicates in prop. This function + ensures * that the theorem prover cannot prove the inconsistency of any of the * new iters in + the result. *) let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst : Predicates.offset list Prop.prop_iter list = let rec root_typ_of_offsets = function @@ -1369,9 +1361,9 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc = raise (Exceptions.Null_dereference (err_desc, __POS__)) -(** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ]. - It returns an iterator with [lexp |-> strexp: typ] as current predicate - and the path (an [offsetlist]) which leads to [lexp] as the iterator state. *) +(** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ]. It returns an + iterator with [lexp |-> strexp: typ] as current predicate and the path (an [offsetlist]) which + leads to [lexp] as the iterator state. *) let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc : Predicates.offset list Prop.prop_iter list = let nlexp = diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 9da2bb490..a37ab1c70 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -6,8 +6,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd (** Interprocedural footprint analysis *) @@ -47,25 +45,19 @@ type valid_res = ; vr_cons_res: (Prop.normal Prop.t * Paths.Path.t) list (** consistent result props *) ; vr_incons_res: (Prop.normal Prop.t * Paths.Path.t) list (** inconsistent result props *) } -(** Result of (bi)-abduction on a single spec. - A result is invalid if no splitting was found, - or if combine failed, or if we are in re - execution mode and the sigma - part of the splitting is not empty. - A valid result contains the missing pi ans sigma, as well as the resulting props. *) +(** Result of (bi)-abduction on a single spec. A result is invalid if no splitting was found, or if + combine failed, or if we are in re - execution mode and the sigma part of the splitting is not + empty. A valid result contains the missing pi ans sigma, as well as the resulting props. *) type abduction_res = | Valid_res of valid_res (** valid result for a function cal *) | Invalid_res of invalid_res (** reason for invalid result *) -(**************** printing functions ****************) - let print_results tenv actual_pre results = L.d_strln "***** RESULTS FUNCTION CALL *******" ; Propset.d actual_pre (Propset.from_proplist tenv results) ; L.d_strln "***** END RESULTS FUNCTION CALL *******" -(***************) - let get_specs_from_payload summary = Option.map summary.Summary.payloads.biabduction ~f:(fun BiabductionSummary.{preposts} -> preposts) |> BiabductionSummary.get_specs_from_preposts @@ -102,8 +94,8 @@ let spec_rename_vars pname spec = BiabductionSummary.{pre= pre''; posts= posts''; visited= spec.BiabductionSummary.visited} -(** Find and number the specs for [proc_name], - after renaming their vars, and also return the parameters *) +(** Find and number the specs for [proc_name], after renaming their vars, and also return the + parameters *) let spec_find_rename summary : (int * Prop.exposed BiabductionSummary.spec) list * Pvar.t list = let proc_name = Summary.get_proc_name summary in try @@ -127,10 +119,9 @@ let spec_find_rename summary : (int * Prop.exposed BiabductionSummary.spec) list (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) -(** Process a splitting coming straight from a call to the prover: - change the instantiating substitution so that it returns primed vars, - except for vars occurring in the missing part, where it returns - footprint vars. *) +(** Process a splitting coming straight from a call to the prover: change the instantiating + substitution so that it returns primed vars, except for vars occurring in the missing part, + where it returns footprint vars. *) let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld frame_typ missing_typ = let hpred_has_only_footprint_vars hpred = @@ -268,8 +259,8 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ ; missing_typ= norm_missing_typ } -(** Check whether an inst represents a dereference without null check, - and return the line number and path position *) +(** Check whether an inst represents a dereference without null check, and return the line number + and path position *) let find_dereference_without_null_check_in_inst = function | Predicates.Iupdate (Some true, _, n, pos) | Predicates.Irearrange (Some true, _, n, pos) -> Some (n, pos) @@ -277,8 +268,8 @@ let find_dereference_without_null_check_in_inst = function None -(** Check whether a sexp contains a dereference without null check, - and return the line number and path position *) +(** Check whether a sexp contains a dereference without null check, and return the line number and + path position *) let rec find_dereference_without_null_check_in_sexp = function | Predicates.Eexp (_, inst) -> find_dereference_without_null_check_in_inst inst @@ -303,8 +294,8 @@ and find_dereference_without_null_check_in_sexp_list = function Some x ) -(** Check dereferences implicit in the spec pre. - In case of dereference error, return [Some(deref_error, description)], otherwise [None] *) +(** Check dereferences implicit in the spec pre. In case of dereference error, return + [Some(deref_error, description)], otherwise [None] *) let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre formal_params = let check_dereference e sexp = let e_sub = Predicates.exp_sub sub e in @@ -418,9 +409,8 @@ let check_path_errors_in_post tenv caller_pname post post_path = List.iter ~f:check_attr (Attribute.get_all post) -(** Post process the instantiated post after the function call so that - x.f |-> se becomes x |-> { f: se }. - Also, update any Aresource attributes to refer to the caller *) +(** Post process the instantiated post after the function call so that [x.f |-> se] becomes + [x |-> { f: se }]. Also, update any Aresource attributes to refer to the caller *) let post_process_post tenv caller_pname callee_pname loc actual_pre ((post : Prop.exposed Prop.t), post_path) = let actual_pre_has_freed_attribute e = @@ -645,9 +635,8 @@ let sigma_star_typ (sigma1 : Predicates.hpred list) (typings2 : (Exp.t * Exp.t) raise (Exceptions.Cannot_star __POS__) -(** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] - extends the footprint of [prop] with [pi,sigma] - and extends the fields of |-> with [missing_fld] *) +(** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] extends the footprint of + [prop] with [pi,sigma] and extends the fields of |-> with [missing_fld] *) let prop_footprint_add_pi_sigma_starfld_sigma tenv (prop : 'a Prop.t) pi_new sigma_new missing_fld missing_typ : Prop.normal Prop.t option = let rec extend_sigma current_sigma new_sigma = @@ -683,8 +672,8 @@ let prop_footprint_add_pi_sigma_starfld_sigma tenv (prop : 'a Prop.t) pi_new sig Some (Prop.normalize tenv (Prop.set prop ~pi:pi' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp'')) -(** Check if the attribute change is a mismatch between a kind - of allocation and a different kind of deallocation *) +(** Check if the attribute change is a mismatch between a kind of allocation and a different kind of + deallocation *) let check_attr_dealloc_mismatch att_old att_new = match (att_old, att_new) with | ( PredSymb.Aresource ({ra_kind= Racquire; ra_res= Rmemory mk_old} as ra_old) @@ -920,9 +909,8 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat Some results -(** Construct the actual precondition: add to the current state a copy - of the (callee's) formal parameters instantiated with the actual - parameters. *) +(** Construct the actual precondition: add to the current state a copy of the (callee's) formal + parameters instantiated with the actual parameters. *) let mk_actual_precondition tenv prop actual_params formal_params = let formals_actuals = let rec comb fpars apars = @@ -1212,9 +1200,8 @@ let remove_constant_string_class tenv prop = Prop.normalize tenv prop' -(** existentially quantify the path identifier generated - by the prover to keep track of expansions of lhs paths - and remove pointsto's whose lhs is a constant string *) +(** existentially quantify the path identifier generated by the prover to keep track of expansions + of lhs paths and remove pointsto's whose lhs is a constant string *) let quantify_path_idents_remove_constant_strings tenv (prop : Prop.normal Prop.t) : Prop.normal Prop.t = let ids_queue = diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 62e9369cd..0abd97801 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd open! AbstractDomain.Types module F = Format @@ -38,10 +36,8 @@ end module SymLinear = struct module M = Symb.SymbolMap - (** - Map from symbols to integer coefficients. - { x -> 2, y -> 5 } represents the value 2 * x + 5 * y - *) + (** Map from symbols to integer coefficients. [{ x -> 2, y -> 5 }] represents the value + [2 * x + 5 * y] *) type t = NonZeroInt.t M.t [@@deriving compare] let empty : t = M.empty @@ -179,7 +175,8 @@ module SymLinear = struct let big_int_ub x = if is_le_zero x then Some Z.zero else None - (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *) + (** When two following symbols are from the same path, simplify what would lead to a zero sum. + E.g. 2 * x.lb - x.ub = x.lb *) let simplify_bound_ends_from_paths : t -> t = fun x -> let f (prev_opt, to_add) symb coeff = @@ -232,11 +229,11 @@ module Bound = struct | Linear of Z.t * SymLinear.t (** [Linear (c, se)] represents [c+se] where [se] is Σ(c⋅x). *) | MinMax of Z.t * Sign.t * MinMax.t * Z.t * Symb.Symbol.t - (** [MinMax] represents a bound of "int [+|-] [min|max](int, symbol)" format. For example, + (** [MinMax] represents a bound of "int [+|-] [min|max](int, symbol)" format. For example, [MinMax (1, Minus, Max, 2, s)] represents [1-max(2,s)]. *) | MinMaxB of MinMax.t * t * t (** [MinMaxB] represents a min/max of two bounds. *) | MultB of Z.t * t * t - (** [MultB] represents a multiplication of two bounds. For example, [MultB (1, x, y)] + (** [MultB] represents a multiplication of two bounds. For example, [MultB (1, x, y)] represents [1 + x × y]. *) | PInf (** +oo *) [@@deriving compare] @@ -1057,7 +1054,8 @@ module Bound = struct let are_similar b1 b2 = Symb.SymbolSet.equal (get_symbols b1) (get_symbols b2) - (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *) + (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as + possible according to [subst_pos]. *) let rec subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted = let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted = fun f x -> match x with Bottom -> Bottom | NonBottom x -> NonBottom (f x) @@ -1291,7 +1289,8 @@ module BoundTrace = struct let of_loop location = Loop location end -(** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) +(** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a + non-negative value once instantiated *) module NonNegativeBound = struct type t = Bound.t * BoundTrace.t [@@deriving compare] diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 486ad85be..939f6bcc8 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd open! AbstractDomain.Types module Bound = Bounds.Bound @@ -177,35 +175,38 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct |> PartialOrder.container ~fold:fold_no_key ~xcompare_elt:(PartialOrder.of_opt ~xcompare_elt) end - (** If x < y < z then - 2 + 3 * x + 4 * x ^ 2 + x * y + 7 * y ^ 2 * z - is represented by - {const= 2; terms= { - x -> {const= 3; terms= { - x -> {const= 4; terms={}}, - y -> {const= 1; terms={}} - }}, - y -> {const= 0; terms= { - y -> {const= 0; terms= { - z -> {const= 7; terms={}} + (** If x < y < z then [2 + 3 * x + 4 * x ^ 2 + x * y + 7 * y ^ 2 * z] is represented by + + {[ + {const= 2; terms= { + x -> {const= 3; terms= { + x -> {const= 4; terms={}}, + y -> {const= 1; terms={}} + }}, + y -> {const= 0; terms= { + y -> {const= 0; terms= { + z -> {const= 7; terms={}} + }} + }} }} - }} - }} - - The representation is a tree, each edge from a node to a child (terms) represents a multiplication by a symbol. If a node has a non-zero const, it represents the multiplication (of the path) by this constant. - In the example above, we have the following paths: - 2 - x * 3 - x * x * 4 - x * y * 1 - y * y * z * 7 - - Invariants: - - except for the root, terms <> {} \/ const <> 0 + ]} + + The representation is a tree, each edge from a node to a child (terms) represents a + multiplication by a symbol. If a node has a non-zero const, it represents the multiplication + (of the path) by this constant. In the example above, we have the following paths: + + - [2] + - [x * 3] + - [x * x * 4] + - [x * y * 1] + - [y * y * z * 7] + + Invariants: + + - except for the root, [terms <> {} || const <> 0] - symbols children of a term are 'smaller' than its self symbol - contents of terms are not zero - - symbols in terms are only symbolic values - *) + - symbols in terms are only symbolic values *) type t = {const: NonNegativeInt.t; terms: t M.t} [@@deriving compare] let of_non_negative_int : NonNegativeInt.t -> t = fun const -> {const; terms= M.empty} diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli index c2d4c5d54..b9305c0bf 100644 --- a/infer/src/checkers/accessPathDomains.mli +++ b/infer/src/checkers/accessPathDomains.mli @@ -20,11 +20,11 @@ module Set : sig val of_list : AccessPath.Abs.t list -> t val mem : AccessPath.Abs.t -> t -> bool - (** return true if {% \gamma(\{ap\}) \subseteq \gamma(aps) %}. note: this is worst-case linear in - the size of the set *) + (** return true if [\gamma(\{ap\}) \subseteq \gamma(aps)]. note: this is worst-case linear in the + size of the set *) val mem_fuzzy : AccessPath.Abs.t -> t -> bool - (** more permissive version of [mem]; return true if {% \gamma(\{a\}) \cap \gamma(aps) != \{\} %}. + (** more permissive version of [mem]; return true if [\gamma(\{a\}) \cap \gamma(aps) != \{\}]. note: this is worst-case linear in the size of the set *) val add : AccessPath.Abs.t -> t -> t diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index 85ed33778..25b499237 100644 --- a/infer/src/checkers/accessTree.mli +++ b/infer/src/checkers/accessTree.mli @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd (** tree of (trace, access path) associations organized by structure of access paths *) @@ -24,19 +22,19 @@ module type S = sig (** map from access -> nodes. a leaf is encoded as an empty map *) | Star (** special leaf for starred access paths *) - (** map from base var -> access subtree. Here's how to represent a few different kinds of - trace * access path associations: {[ - (x, T) := { x |-> (T, Subtree {}) } - (x.f, T) := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) } - (x*, T) := { x |-> (T, Star) } - (x.f*, T) := { x |-> (empty, Subtree { f |-> (T, Star) }) } - (x, T1), (y, T2) := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) } - (x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}), - g |-> (T2, Subtree {}) }) } - ]} - *) - 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: + + {[ + (x, T) := { x |-> (T, Subtree {}) } + (x.f, T) := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) } + (x*, T) := { x |-> (T, Star) } + (x.f*, T) := { x |-> (empty, Subtree { f |-> (T, Star) }) } + (x, T1), (y, T2) := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) } + (x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}), + g |-> (T2, Subtree {}) }) } + ]} *) val empty_node : node diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 24248a6f1..78fadaea3 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd open PolyVariantEqual @@ -18,10 +16,8 @@ module L = Logging module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = struct (** Returns the procname and whether is instance, according to the selector information and - according to the method signature with the following priority: - 1. method is a predefined model - 2. method is found by clang's resolution - 3. Method is found by our resolution *) + according to the method signature with the following priority: 1. method is a predefined model + 2. method is found by clang's resolution 3. Method is found by our resolution *) let get_callee_objc_method context obj_c_message_expr_info callee_ms_opt act_params = let open CContext in let selector, mc_type = CMethod_trans.get_objc_method_data obj_c_message_expr_info in @@ -148,9 +144,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s typ - (** Execute translation and then possibly adjust the type of the result of translation: - In C++, when expression returns reference to type T, it will be lvalue to T, not T&, but - infer needs it to be T& *) + (** Execute translation and then possibly adjust the type of the result of translation: In C++, + when expression returns reference to type T, it will be lvalue to T, not T&, but infer needs + it to be T& *) let exec_with_glvalue_as_reference f trans_state stmt = let expr_info = match Clang_ast_proj.get_expr_tuple stmt with @@ -172,8 +168,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** Execute translation of e forcing to release priority (if it's not free) and then setting it - back. This is used in conditional operators where we need to force the priority to be free for - the computation of the expressions*) + back. This is used in conditional operators where we need to force the priority to be free for + the computation of the expressions*) let exec_with_priority_exception trans_state e f = if PriorityNode.is_priority_free trans_state then f trans_state e else f {trans_state with priority= Free} e @@ -321,10 +317,10 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** FROM CLANG DOCS: "Implements the GNU __null extension, which is a name for a null pointer - constant that has integral type (e.g., int or long) and is the same size and alignment as a - pointer. The __null extension is typically only used by system headers, which define NULL as - __null in C++ rather than using 0 (which is an integer that may not match the size of a - pointer)". So we implement it as the constant zero *) + constant that has integral type (e.g., int or long) and is the same size and alignment as a + pointer. The __null extension is typically only used by system headers, which define NULL as + __null in C++ rather than using 0 (which is an integer that may not match the size of a + pointer)". So we implement it as the constant zero *) let gNUNullExpr_trans trans_state expr_info = let typ = CType_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in let exp = Exp.Const (Const.Cint IntLit.zero) in @@ -391,9 +387,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s mk_trans_result (zero, typ) empty_control - (** Create instructions to initialize record with zeroes. It needs to traverse - whole type structure, to assign 0 values to all transitive fields because of - AST construction in C translation *) + (** Create instructions to initialize record with zeroes. It needs to traverse whole type + structure, to assign 0 values to all transitive fields because of AST construction in C + translation *) let implicitValueInitExpr_trans trans_state stmt_info = match trans_state.var_exp_typ with | Some var_exp_typ -> @@ -1189,7 +1185,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s and cxx_destructor_call_trans trans_state si this_res_trans class_type_ptr ~is_injected_destructor ~is_inner_destructor = - (* cxx_method_construct_call_trans claims a priority with the same `si`. A new pointer is + (* cxx_method_construct_call_trans claims a priority with the same [si]. A new pointer is generated to avoid premature node creation *) let si' = {si with Clang_ast_t.si_pointer= CAst_utils.get_fresh_pointer ()} in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state si' in @@ -1268,7 +1264,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** If the first argument of the call is self in a static context, remove it as an argument and - change the call from instance to static *) + change the call from instance to static *) and objCMessageExpr_translate_args trans_state_param args obj_c_message_expr_info callee_ms_opt = match args with | stmt :: rest -> ( @@ -1387,7 +1383,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let bases = match typ_pointer_opt with Some p -> bases @ [p] | None -> bases in let _, sloc2 = stmt_info.Clang_ast_t.si_source_range in let stmt_info_loc = {stmt_info with Clang_ast_t.si_source_range= (sloc2, sloc2)} in - (* compute `this` once that is used for all destructor calls of virtual base class *) + (* compute [this] once that is used for all destructor calls of virtual base class *) let obj_sil, this_qual_type, this_res_trans = compute_this_expr trans_state stmt_info_loc in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info_loc in let bases_res_trans = @@ -1417,9 +1413,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let bases = CAst_utils.get_cxx_base_classes decl in let _, sloc2 = stmt_info.Clang_ast_t.si_source_range in let stmt_info_loc = {stmt_info with Clang_ast_t.si_source_range= (sloc2, sloc2)} in - (* compute `this` once that is used for all destructors of fields and base classes *) + (* compute [this] once that is used for all destructors of fields and base classes *) let obj_sil, this_qual_type, this_res_trans = compute_this_expr trans_state stmt_info_loc in - (* ReturnStmt claims a priority with the same `stmt_info`. + (* ReturnStmt claims a priority with the same [stmt_info]. New pointer is generated to avoid premature node creation *) let stmt_info' = {stmt_info_loc with Clang_ast_t.si_pointer= CAst_utils.get_fresh_pointer ()} @@ -1468,7 +1464,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (* The source location of destructor should reflect the end of the statement *) let _, sloc2 = stmt_info.Clang_ast_t.si_source_range in let stmt_info_loc = {stmt_info with Clang_ast_t.si_source_range= (sloc2, sloc2)} in - (* ReturnStmt claims a priority with the same `stmt_info`. + (* ReturnStmt claims a priority with the same [stmt_info]. New pointer is generated to avoid premature node creation *) let stmt_info' = {stmt_info_loc with Clang_ast_t.si_pointer= CAst_utils.get_fresh_pointer ()} @@ -1609,8 +1605,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s assert false - (** The GNU extension to the conditional operator which allows the middle operand to be - omitted. *) + (** The GNU extension to the conditional operator which allows the middle operand to be omitted. *) and binaryConditionalOperator_trans trans_state stmt_info stmt_list expr_info = match stmt_list with | [stmt1; ostmt1; ostmt2; stmt2] @@ -1646,8 +1641,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** Translate a condition for if/loops statement. It shorts-circuit and/or. The invariant is that - the translation of a condition always contains (at least) the prune nodes. Moreover these are - always the leaf nodes of the translation. *) + the translation of a condition always contains (at least) the prune nodes. Moreover these are + always the leaf nodes of the translation. *) and cond_trans ~if_kind ~negate_cond trans_state cond : trans_result = let context = trans_state.context in let cond_source_range = source_range_of_stmt cond in @@ -1667,12 +1662,12 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (* Assumption: If it's a null_stmt, it is a loop with no bound, so we set condition to 1 *) else if is_cmp then let open Clang_ast_t in - (* If we have a comparision here, do not dispatch it to `instruction` function, which + (* If we have a comparision here, do not dispatch it to [instruction] function, which * invokes binaryOperator_trans_with_cond -> conditionalOperator_trans -> cond_trans. * This will throw the translation process into an infinite loop immediately. * Instead, dispatch to binaryOperator_trans directly. *) - (* If one wants to add a new kind of `BinaryOperator` that will have the same behavior, - * she need to change both the codes here and the `match` in + (* If one wants to add a new kind of [BinaryOperator] that will have the same behavior, + * she need to change both the codes here and the [match] in * binaryOperator_trans_with_cond *) match cond with | BinaryOperator (si, ss, ei, boi) @@ -2142,21 +2137,20 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s loop_instruction trans_state dowhile_kind stmt_info - (** Iteration over collection - - for (v : C) { body; } + (** Iteration over collections - is translated as follows: + [for (v : C) { body; }] is translated as: - TypeC __range = C; - for (__begin = __range.begin(), __end = __range.end(); - __begin != __end; - ++__begin) - { - v = *__begin; - loop_body; - } - *) + {[ + TypeC __range = C; + for (__begin = __range.begin(), __end = __range.end(); + __begin != __end; + ++__begin) + { + v = *__begin; + loop_body; + } + ]} *) and cxxForRangeStmt_trans trans_state stmt_info stmt_list = let open Clang_ast_t in match stmt_list with @@ -2183,14 +2177,14 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s assert false - (** Fast iteration for colection - for (type_it i in collection) { body } - is translate as - { - i = type_next_object(); - while(i != nil) { body; i = type_next_object();} - } - *) + (** Fast iteration for collections + + [for (type_it i in collection) { body }] is translated as + + {[ + i = type_next_object(); + while(i != nil) { body; i = type_next_object();} + ]} *) and objCForCollectionStmt_trans trans_state item items body stmt_info = ignore (instruction trans_state item) ; (* Here we do ast transformation, so we don't need the value of the translation of the *) @@ -2265,12 +2259,13 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** InitListExpr can have following meanings: + - initialize all record fields - initialize array - initialize primitive type (int/flaot/pointer/...) - - perform zero initalization - http://en.cppreference.com/w/cpp/language/zero_initialization - Decision which case happens is based on the type of the InitListExpr - *) + - perform zero initalization - + {:http://en.cppreference.com/w/cpp/language/zero_initialization} Decision which case happens + is based on the type of the InitListExpr *) and initListExpr_trans trans_state stmt_info expr_info stmts = let var_exp, var_typ = match trans_state.var_exp_typ with @@ -2493,24 +2488,24 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s "Expected source expression for OpaqueValueExpr" ) - (* NOTE: This translation has several hypothesis. Need to be verified when we have more*) - (* experience with this construct. Assert false will help to see if we encounter programs*) - (* that do not conform with this hypothesis.*) - (* Hypotheses:*) - (* 1. stmt_list is composed by 2 parts: the first element is a syntactic description of the*) - (* expression. The rest of the list has a semantic caracterization of the expression and*) - (* defines how that expression is going to be implemented at runtime. *) - (* 2. the semantic description is composed by a list of OpaqueValueExpr that define the *) - (* various expressions involved and one finale expression that define how the final value of*) - (* the PseudoObjectExpr is obtained. - All the OpaqueValueExpr will be part of the last expression.*) - (* So they can be skipped. *) - (* For example: 'x.f = a' when 'f' is a property will be - translated with a call to f's setter [x f:a]*) - (* the stmt_list will be [x.f = a; x; a; CallToSetter] - Among all element of the list we only need*) - (* to translate the CallToSetter which is - how x.f = a is actually implemented by the runtime.*) + (** NOTE: This translation has several hypothesis. Need to be verified when we have more + experience with this construct. [assert false] will help to see if we encounter programs that + do not conform with this hypothesis. + + Hypotheses: + + + [stmt_list] is composed of 2 parts: the first element is a syntactic description of the + expression. The rest of the list has a semantic caracterization of the expression and + defines how that expression is going to be implemented at runtime. + + The semantic description is composed by a list of OpaqueValueExpr that define the various + expressions involved and one finale expression that define how the final value of the + PseudoObjectExpr is obtained. + + All the OpaqueValueExpr will be part of the last expression. So they can be skipped. For + example: [x.f = a] when [f] is a property will be translated with a call to [f]'s setter + [x f:a] the [stmt_list] will be [x.f = a; x; a; CallToSetter]. Among all element of the list + we only need to translate the CallToSetter which is how [x.f = a] is actually implemented by + the runtime.*) and pseudoObjectExpr_trans trans_state stmt_list = L.(debug Capture Verbose) " priority node free = '%s'@\n@\n" @@ -2645,8 +2640,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s cxx_inject_field_destructors_in_destructor_body trans_state_pri stmt_info else None in - (* `cxx_inject_field_destructors_in_destructor_body` should not create new nodes for return statement, - this is ensured by creating a fresh pointer in `cxx_inject_field_destructors_in_destructor_body` + (* [cxx_inject_field_destructors_in_destructor_body] should not create new nodes for return statement, + this is ensured by creating a fresh pointer in [cxx_inject_field_destructors_in_destructor_body] *) check_destructor_translation destructor_res ; let instrs_of = function Some {control= {instrs}} -> instrs | None -> [] in @@ -3395,7 +3390,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** inject destructors at the end of the translation of the statement if the context map says - there are variables to destruct *) + there are variables to destruct *) and instruction_scope trans_state stmt = let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in let destr_trans_result = @@ -3783,8 +3778,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s trans_state stmt_info ret_typ stmts - (** Function similar to instruction function, but it takes C++ constructor initializer as - an input parameter. *) + (** Function similar to instruction function, but it takes C++ constructor initializer as an input + parameter. *) and cxx_constructor_init_trans ctor_init trans_state = let context = trans_state.context in let source_range = ctor_init.Clang_ast_t.xci_source_range in @@ -3804,8 +3799,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s match ctor_init.Clang_ast_t.xci_subject with | `Delegating _ | `BaseClass _ -> let this_exp, this_typ = this_res_trans.return in - (* Hack: Strip pointer from type here since cxxConstructExpr_trans expects it this way *) - (* it will add pointer back before making it a parameter to a call *) + (* Hack: Strip pointer from type here since cxxConstructExpr_trans expects it this way + it will add pointer back before making it a parameter to a call *) let class_typ = match this_typ.Typ.desc with Tptr (t, _) -> t | _ -> assert false in {this_res_trans with return= (this_exp, class_typ)} | `Member decl_ref -> diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 546ea5cc6..858654e78 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -51,7 +51,7 @@ module ThreadsDomain : sig locks, etc.) *) | AnyThreadButSelf (** Current thread can run in parallel with other threads, but not with a copy of itself. - (concretization : {% \{ t | t \in TIDs ^ t != t_cur \} %} ) *) + (concretization : [{ t | t \in TIDs && t != t_cur }]) *) | AnyThread (** Current thread can run in parallel with any thread, including itself (concretization: set of all TIDs ) *) diff --git a/infer/src/cost/costDomain.ml b/infer/src/cost/costDomain.ml index 44f0f6849..e3e854a6c 100644 --- a/infer/src/cost/costDomain.ml +++ b/infer/src/cost/costDomain.ml @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd module F = Format @@ -18,11 +16,9 @@ module BasicCost = struct let version = 5 end -(** - Module to simulate a record - {OperationCost:BasicCost.t; AllocationCost: BasicCost.t; IOCost:BasicCost.t} with a map - {OperationCost, AllocationCost, IOCost} -> BasicCost.t -*) +(** Module to simulate a record + [{OperationCost:BasicCost.t; AllocationCost: BasicCost.t; IOCost:BasicCost.t}] with a map + [{OperationCost, AllocationCost, IOCost} -> BasicCost.t] *) module VariantCostMap = struct include PrettyPrintable.PPMonoMapOfPPMap (CostIssues.CostKindMap) (BasicCost) diff --git a/infer/src/cost/costDomain.mli b/infer/src/cost/costDomain.mli index 1e39dd7b0..996d84ab5 100644 --- a/infer/src/cost/costDomain.mli +++ b/infer/src/cost/costDomain.mli @@ -36,7 +36,7 @@ val get_operation_cost : t -> BasicCost.t val map : f:(BasicCost.t -> BasicCost.t) -> t -> t val zero_record : t -(** Map representing cost record {OperationCost:0; AllocationCost:0; IOCost:0} *) +(** Map representing cost record \{OperationCost:0; AllocationCost:0; IOCost:0\} *) val mult_by : t -> nb_exec:BasicCost.t -> t (** Special map where each element is multiplied by the number of executions *) @@ -45,10 +45,10 @@ val plus : t -> t -> t (** Union of two maps where common costs are added together *) val unit_cost_atomic_operation : t -(** Map representing cost record {OperationCost:1; AllocationCost:0; IOCost:0} *) +(** Map representing cost record \{OperationCost:1; AllocationCost:0; IOCost:0\} *) val unit_cost_allocation : t -(** Map representing cost record {OperationCost:0; AllocationCost:1; IOCost:0} *) +(** Map representing cost record \{OperationCost:0; AllocationCost:1; IOCost:0\} *) val of_operation_cost : BasicCost.t -> t -(** Map representing cost record {OperationCost:operation_cost; AllocationCost:0; IOCost:0} *) +(** Map representing cost record \{OperationCost:operation_cost; AllocationCost:0; IOCost:0\} *) diff --git a/infer/src/scuba/ScubaLogging.mli b/infer/src/scuba/ScubaLogging.mli index 9f7559b21..dd6300f18 100644 --- a/infer/src/scuba/ScubaLogging.mli +++ b/infer/src/scuba/ScubaLogging.mli @@ -5,35 +5,26 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd -(** - Functionality for logging into "infer_events" Scuba table. - The table is organized in form of key-value pairs. - Two most important fields are "event" and "value". - Other fields in the table correspond to things common for this particular - run of Infer. - *) +(** Functionality for logging into "infer_events" Scuba table. The table is organized in form of + key-value pairs. Two most important fields are "event" and "value". Other fields in the table + correspond to things common for this particular run of Infer. *) val log_many : LogEntry.t list -> unit -(** Log several events in one go. Useful when you do custom aggregations - and have a place to log all aggregated results at once. - *) +(** Log several events in one go. Useful when you do custom aggregations and have a place to log all + aggregated results at once. *) val log_count : label:string -> value:int -> unit (** Log anything that can be counted. Events will be prefixed with "count." *) val execute_with_time_logging : string -> (unit -> 'a) -> 'a -(** - A helper to log execution time of a particular function. - Use this to measure a performance of a given function. - Example: - {| +(** A helper to log execution time of a particular function. Use this to measure a performance of a + given function. Example: + + {[ let f a b = let f a b = ScubaLogging.execute_with_time_logging "f" (fun () -> f a b) - |} - *) + ]} *) val register_global_log_flushing_at_exit : unit -> unit