From a50673c13744c20c392d3edabd33ae0a534b088d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 11 May 2022 17:48:41 +0200
Subject: [PATCH] [doc] various line break fixes
---
src/kernel_services/abstract_interp/int_set.mli | 6 +++---
src/kernel_services/analysis/stmts_graph.mli | 14 +++++++-------
src/kernel_services/ast_data/cil_types.mli | 5 +++--
.../ast_data/property_status.mli | 3 ++-
src/kernel_services/ast_queries/cil.mli | 2 +-
.../ast_queries/cil_builtins.mli | 2 +-
src/kernel_services/ast_queries/cil_const.mli | 17 ++++++++---------
src/libraries/project/state_builder.mli | 4 +++-
src/libraries/stdlib/extlib.mli | 3 ++-
src/libraries/utils/bitvector.mli | 2 ++
src/plugins/e-acsl/src/libraries/functions.mli | 6 +++---
src/plugins/pdg/annot.mli | 6 ++----
src/plugins/pdg/ctrlDpds.mli | 2 +-
src/plugins/slicing/fct_slice.mli | 6 +++---
src/plugins/slicing/slicingMarks.mli | 2 +-
src/plugins/sparecode/Sparecode.mli | 12 ++++++------
src/plugins/wp/Lang.mli | 4 ++--
17 files changed, 50 insertions(+), 46 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index d3aac28587c..979dfbe883a 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 e7e0eeaa9ed..22bf4c70599 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 28e7ce49ef6..bb4b6ae4d04 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 1ac60ebf9d0..92f57d7ad44 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 8d67ee88685..7cbbdfbc67f 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 ebbebbbde4d..d48b61b1f89 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 bc7db0a6014..ff5c455d9a7 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 94f4dc217b4..c3a630b794a 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 6eac85cefbc..d736864c0c4 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 63346ddbde8..d240d817e90 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 01132f08a85..97667d9b194 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 9004f92ddb7..8aa29637584 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 0f00964488b..184bc56aedc 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 b05520e7f73..6ea3a114edb 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 7081adb36a8..d398c3967fd 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 2f2b503634d..66d9defb721 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 f93ec5f6fb1..0543fe9195f 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 } *)
--
GitLab