[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
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent c1818c0c1c
commit acb76469b5

@ -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

@ -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

@ -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 *)

@ -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 *)
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 *)
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 *)

@ -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 =

@ -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

@ -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. *)

@ -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 =

@ -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 =

@ -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 =
@ -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]

@ -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,9 +175,9 @@ 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
(** 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={}},
@ -191,21 +189,24 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
}}
}}
}}
]}
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:
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
- [2]
- [x * 3]
- [x * x * 4]
- [x * y * 1]
- [y * y * z * 7]
Invariants:
- except for the root, terms <> {} \/ const <> 0
- 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}

@ -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

@ -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,8 +22,11 @@ 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: {[
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) }
@ -33,10 +34,7 @@ module type S = sig
(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
]} *)
val empty_node : node

@ -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
@ -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
@ -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]
@ -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,12 +2137,11 @@ 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;
@ -2156,7 +2150,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
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
{
(** 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
@ -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 ->

@ -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 ) *)

@ -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)

@ -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\} *)

@ -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 = <some code>
let f a b = ScubaLogging.execute_with_time_logging "f" (fun () -> f a b)
|}
*)
]} *)
val register_global_log_flushing_at_exit : unit -> unit

Loading…
Cancel
Save