diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli index d3aac28587ccc2bf78c127d5710a0a4cc4501fba..979dfbe883a48f9d001ff300c38acfe361cec076 100644 --- a/src/kernel_services/abstract_interp/int_set.mli +++ b/src/kernel_services/abstract_interp/int_set.mli @@ -45,9 +45,9 @@ include Datatype.S_with_collections (** Creates the set containing only the given integer. *) val inject_singleton: Integer.t -> t -(** Creates the set with integers [from + k*period] for [k] in {0 ... number-1}. - The resulting set contains [number] integers. There is no verification - about [number], but it should be stritly positive. *) +(** Creates the set with integers [from + k*period] for [k] in + [{0 ... number-1}]. The resulting set contains [number] integers. There is + no verification about [number], but it should be stritly positive. *) val inject_periodic: from:Integer.t -> period:Integer.t -> number:Integer.t -> t (** Creates a set from an integer list. The list must not be empty, and the list diff --git a/src/kernel_services/analysis/stmts_graph.mli b/src/kernel_services/analysis/stmts_graph.mli index e7e0eeaa9ed6fa757e8e65b6007a930df4d7653a..22bf4c705996d6729079c276c32ec4a9ecdc5b25 100644 --- a/src/kernel_services/analysis/stmts_graph.mli +++ b/src/kernel_services/analysis/stmts_graph.mli @@ -69,17 +69,17 @@ val get_stmt_last_stmts : termination_kind option -> stmt -> stmt list val get_block_last_stmts : termination_kind option -> block -> stmt list (** Find the entry edges that go inside [s] statements, - * meaning that if the pair [(s1,s2)] is in the returned information, - * [s2] is a successor of [s1] and [s2] is in [s] statements, but [s1] is not. - * @since Nitrogen-20111001 - **) + meaning that if the pair [(s1,s2)] is in the returned information, + [s2] is a successor of [s1] and [s2] is in [s] statements, but [s1] is not. + @since Nitrogen-20111001 +*) val get_stmt_in_edges : stmt -> (stmt * stmt) list val get_block_in_edges : block -> (stmt * stmt) list (** Like [get_stmt_in_edges] but for edges going out of [s] statements. - * Similar to [get_all_stmt_last_stmts] but gives the edge information - * instead of just the first statement. - * @since Nitrogen-20111001 + Similar to [get_all_stmt_last_stmts] but gives the edge information + instead of just the first statement. + @since Nitrogen-20111001 *) val get_all_stmt_out_edges : stmt -> (stmt * stmt) list val get_all_block_out_edges : block -> (stmt * stmt) list diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli index 28e7ce49ef681900375afdce3a27b3a91e361f51..bb4b6ae4d041ed3a706aa06b4c4ce3390f096b02 100644 --- a/src/kernel_services/ast_data/cil_types.mli +++ b/src/kernel_services/ast_data/cil_types.mli @@ -787,7 +787,7 @@ and binop = (** Left values (aka Lvalues) are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator. In C the syntax for lvalues is not always a good indication of the meaning of the - lvalue. For example the C value {v a[0][1][2] v} might involve 1, 2 or 3 + lvalue. For example the C value [a[0][1][2]] might involve 1, 2 or 3 memory reads when used in an expression context, depending on the declared type of the variable [a]. If [a] has type [int \[4\]\[4\]\[4\]] then we have one memory read from somewhere inside the area that stores the array [a]. On @@ -822,7 +822,8 @@ and binop = - {!Cil.removeOffset} and {!Cil.removeOffsetLval} - shrink sequences of offsets. - The following equivalences hold {v + The following equivalences hold + {v Mem(AddrOf(Mem a, aoff)), off = Mem a, aoff + off Mem(AddrOf(Var v, aoff)), off = Var v, aoff + off AddrOf (Mem a, NoOffset) = a diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli index 1ac60ebf9d079e57ad8f043c645738861fc38da5..92f57d7ad4402fb465f7c7048c48e0f0b9bec992 100644 --- a/src/kernel_services/ast_data/property_status.mli +++ b/src/kernel_services/ast_data/property_status.mli @@ -68,7 +68,8 @@ val emit: the best status is changed accordingly. One example when [~distinct:true] may be required is when emitting a status for a pre-condition of a function [f] since the status associated to a pre-condition [p] merges all statuses - of [p] at each callsite of the function [f]. @return the kept status. + of [p] at each callsite of the function [f]. + @return the kept status. @raise Inconsistent_emitted_status when emitting False after emitting True or conversely *) diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 8d67ee88685af49156bd0db736a208211b7f8418..7cbbdfbc67f17124077a61c2bf0ba574af659796 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -2041,7 +2041,7 @@ val is_empty_funspec: funspec -> bool val is_empty_behavior: funbehavior -> bool (* ************************************************************************* *) -(** {2 ALPHA conversion} has been moved to the Alpha module. *) +(** {2 ALPHA conversion has been moved to the Alpha module} *) (* ************************************************************************* *) (** Assign unique names to local variables. This might be necessary after you diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli index ebbebbbde4dfe3bb30cb2f4f8eb59d258aafbc16..d48b61b1f898d7e770e539e366bf8ed31b696505 100644 --- a/src/kernel_services/ast_queries/cil_builtins.mli +++ b/src/kernel_services/ast_queries/cil_builtins.mli @@ -49,7 +49,7 @@ open Cil_types (** This module associates the name of a built-in function that might be used during elaboration with the corresponding varinfo. This is done when - parsing ${FRAMAC_SHARE}/libc/__fc_builtins.h, which is always performed + parsing [${FRAMAC_SHARE}/libc/__fc_builtins.h], which is always performed before processing the actual list of files provided on the command line (see {!File.init_from_c_files}). Actual list of such built-ins is managed in {!Cabs2cil}. *) diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli index bc7db0a6014b200a8c553af918149ded974959a4..ff5c455d9a7dd4af62a63aa59d3ad991ac3aef30 100644 --- a/src/kernel_services/ast_queries/cil_const.mli +++ b/src/kernel_services/ast_queries/cil_const.mli @@ -74,15 +74,14 @@ val new_raw_id: unit -> int Must not be used for setting vid: use {!set_vid} instead. *) (** Creates a (potentially recursive) composite type. The arguments are: - * (1) a boolean indicating whether it is a struct or a union, (2) the name - * (always non-empty), (3) a function that when given a representation of the - * structure type constructs the type of the fields recursive type (the first - * argument is only useful when some fields need to refer to the type of the - * structure itself), and (4) an optional list of attributes to be associated - * with the composite type, "None" means that the struct is incomplete. - * - * @since 23.0-Vanadium the 4th parameter is a function that returns an option. - **) + (1) a boolean indicating whether it is a struct or a union, (2) the name + (always non-empty), (3) a function that when given a representation of the + structure type constructs the type of the fields recursive type (the first + argument is only useful when some fields need to refer to the type of the + structure itself), and (4) an optional list of attributes to be associated + with the composite type, "None" means that the struct is incomplete. + @since 23.0-Vanadium the 4th parameter is a function that returns an option. +*) val mkCompInfo: bool -> (* whether it is a struct or a union *) string -> (* name of the composite type; cannot be empty *) ?norig:string -> (* original name of the composite type, empty when anonymous *) diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli index 94f4dc217b4c43f71e87506304b4672ad70d7a8c..c3a630b794a3869907eeaf8819e7a541622ae9f3 100644 --- a/src/libraries/project/state_builder.mli +++ b/src/libraries/project/state_builder.mli @@ -545,7 +545,9 @@ module States: sig (** iterates a function [f] over all registered states. Arguments of [f] are its name, its type value, its value for the given project ([Project.current ()] by default) and a boolean which indicates if it is - already computed. @since Fluorine-20130401 *) + already computed. + @since Fluorine-20130401 + *) val fold: ?prj:Project.t -> diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli index 6eac85cefbcefc87840ff81837a86325286a7e01..d736864c0c471948fc67fd8160f565624b8ccdd7 100644 --- a/src/libraries/stdlib/extlib.mli +++ b/src/libraries/stdlib/extlib.mli @@ -224,7 +224,8 @@ val opt_map2: ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option (* ************************************************************************* *) val xor: bool -> bool -> bool -(** exclusive-or. @since Oxygen-20120901 *) +(** exclusive-or. + @since Oxygen-20120901 *) (* ************************************************************************* *) (** {2 Strings} *) diff --git a/src/libraries/utils/bitvector.mli b/src/libraries/utils/bitvector.mli index 63346ddbde8c182fd7429030c128cfd3d8859e36..d240d817e90c90f22a9ff0287affc8958fe62ed5 100644 --- a/src/libraries/utils/bitvector.mli +++ b/src/libraries/utils/bitvector.mli @@ -55,6 +55,7 @@ val compare: t -> t -> int val hash: t -> int (** {2 Bitwise Binary Operations} + The first argument is the size of the vectors. *) val bnot: int -> t -> t @@ -64,6 +65,7 @@ val bxor: int -> t -> t -> t (* bitwise difference *) val beq: int -> t -> t -> t (* bitwise equivalence/equality *) (** {2 Generic Bitwise Operations}. + Prefer using these rather than create intermediary bitvectors. *) val bitwise_op2: int -> (int -> int -> int) -> t -> t -> t diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli index 01132f08a85a466222da30e5995ea7cae9e64caf..97667d9b1942dfa59e92ffc2082984f840663a21 100644 --- a/src/plugins/e-acsl/src/libraries/functions.mli +++ b/src/plugins/e-acsl/src/libraries/functions.mli @@ -34,7 +34,7 @@ val instrument: kernel_function -> bool (** @return [true] iff the given function must be instrumented. *) (* ************************************************************************** *) -(** {2 RTL} Operations on function belonging to the runtime library of E-ACSL *) +(** {2 RTL Operations on function belonging to the runtime library of E-ACSL} *) (* ************************************************************************** *) module RTL: sig @@ -67,7 +67,7 @@ module RTL: sig end (* Rtl *) (* ************************************************************************** *) -(** {2 Libc} Operations on functions belonging to standard library *) +(** {2 Libc Operations on functions belonging to standard library} *) (* ************************************************************************** *) module Libc: sig @@ -133,7 +133,7 @@ module Libc: sig end (* Libc *) (* ************************************************************************** *) -(** {2 Concurrency} Operations concerning the support of concurrency *) +(** {2 Concurrency Operations concerning the support of concurrency} *) (* ************************************************************************** *) module Concurrency: sig diff --git a/src/plugins/pdg/annot.mli b/src/plugins/pdg/annot.mli index 9004f92ddb798d6bd04ce0e75cd59ec7385156b4..8aa296375843ddb909c61cba30f6b76014ea6c3e 100644 --- a/src/plugins/pdg/annot.mli +++ b/src/plugins/pdg/annot.mli @@ -21,10 +21,8 @@ (**************************************************************************) (** All these functions find the nodes needed for various kind of annotations. - * - * @raise Kernel_function.No_Definition on annotations for function declarations. - * - * *) + @raise Kernel_function.No_Definition on annotations for function declarations. +*) (** [data_info] is composed of [(node,z_part) list, undef_loc)] * and correspond to data dependencies nodes. diff --git a/src/plugins/pdg/ctrlDpds.mli b/src/plugins/pdg/ctrlDpds.mli index 0f00964488be915457a868a2c9c7088c464e1879..184bc56aedc5c90716d4315c068076d963600496 100644 --- a/src/plugins/pdg/ctrlDpds.mli +++ b/src/plugins/pdg/ctrlDpds.mli @@ -35,7 +35,7 @@ val get_if_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t * on the given jump statement. This statement can be a [goto] of course, * but also a [break], a [continue], or even a loop because CIL transformations make them of the form {v while(true) body; v} which is equivalent to - {v L : body ; goto L; v} + [L : body ; goto L;] * *) val get_jump_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t val get_loop_controlled_stmts : t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t diff --git a/src/plugins/slicing/fct_slice.mli b/src/plugins/slicing/fct_slice.mli index b05520e7f73f19e64f0c4652c31bf54f0ce85523..6ea3a114edbdc847d41731dc0d04e4ec1dd20157 100644 --- a/src/plugins/slicing/fct_slice.mli +++ b/src/plugins/slicing/fct_slice.mli @@ -34,9 +34,9 @@ val is_src_fun_visible : Cil_types.kernel_function -> bool (** - * @raise SlicingTypes.ExternalFunction if the function has no source code, - * because there cannot be any slice for it. - * @raise SlicingTypes.NoPdg when there is no PDG for the function. + @raise SlicingTypes.ExternalFunction if the function has no source code, + because there cannot be any slice for it. + @raise SlicingTypes.NoPdg when there is no PDG for the function. *) val make_new_ff : fct_info -> bool -> fct_slice * criterion list diff --git a/src/plugins/slicing/slicingMarks.mli b/src/plugins/slicing/slicingMarks.mli index 7081adb36a8ea736d374db098096bece3413a312..d398c3967fdaec9c47b1e2aa9a4cbd5fc79a47af 100644 --- a/src/plugins/slicing/slicingMarks.mli +++ b/src/plugins/slicing/slicingMarks.mli @@ -40,7 +40,7 @@ val merge_marks : sl_mark list -> sl_mark val inter_marks : sl_mark list -> sl_mark (** [combine_marks] add a new information to the old value. - * @return (new_mark, is_new) + @return (new_mark, is_new) where [is_new=true] if the new mark is not included in the old one. *) val combine_marks : sl_mark -> sl_mark -> (sl_mark * sl_mark) diff --git a/src/plugins/sparecode/Sparecode.mli b/src/plugins/sparecode/Sparecode.mli index 2f2b503634d6963779eee23c1ec856c8e0aa4222..66d9defb721368dfb49a801fd1f7b1af3a1fad7b 100644 --- a/src/plugins/sparecode/Sparecode.mli +++ b/src/plugins/sparecode/Sparecode.mli @@ -27,16 +27,16 @@ module Register: sig val get: select_annot:bool -> select_slice_pragma:bool -> Project.t (** Remove in each function what isn't used to compute its outputs, - * or its annotations when [select_annot] is true, - * or its slicing pragmas when [select_slice_pragmas] is true. - * @return a new project where the sparecode has been removed. + or its annotations when [select_annot] is true, + or its slicing pragmas when [select_slice_pragmas] is true. + @return a new project where the sparecode has been removed. *) val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> Project.t (** Remove unused global types and variables from the given project - * (the current one if no project given). - * The source project is not modified. - * The result is in the returned new project. + (the current one if no project given). + The source project is not modified. + The result is in the returned new project. * *) end diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli index f93ec5f6fb1128aec68241983a17994bf6166476..0543fe9195f382d71ea56a1cc5721ec033d3ab6b 100644 --- a/src/plugins/wp/Lang.mli +++ b/src/plugins/wp/Lang.mli @@ -31,7 +31,7 @@ open Qed.Logic type library = string -(** {2 Naming} Unique identifiers. *) +(** {2 Naming - Unique identifiers} *) val comp_id : compinfo -> string val comp_init_id : compinfo -> string @@ -558,7 +558,7 @@ end module N: sig - (** simpler notation for writing {!F.term} and {F.pred} *) + (** simpler notation for writing {!F.term} and {!F.pred} *) val ( + ): F.binop (** {! F.p_add } *)