diff --git a/src/kernel_internals/typing/cfg.mli b/src/kernel_internals/typing/cfg.mli
index 6c9f98bda9f94b5d7b670a8c9d0e4000d646387f..7a2cd914a7712e2e8241c465e8399a2da36aeb4f 100644
--- a/src/kernel_internals/typing/cfg.mli
+++ b/src/kernel_internals/typing/cfg.mli
@@ -46,7 +46,7 @@
This will fill in the [preds] and [succs] fields of {!Cil_types.stmt}
This is nearly always automatically done by the kernel. You only need
- those functions if you build {!Cil_types.fundec} yourself. *)
+ those functions if you build {!type:Cil_types.fundec} yourself. *)
open Cil_types
diff --git a/src/kernel_internals/typing/populate_spec.mli b/src/kernel_internals/typing/populate_spec.mli
index fa2e95c65c54bacf5fb08e75539327e23989c66a..93f103c6def585bbb5c634821ce2744c842ad27d 100644
--- a/src/kernel_internals/typing/populate_spec.mli
+++ b/src/kernel_internals/typing/populate_spec.mli
@@ -58,7 +58,7 @@ type t_requires = identified_predicate list
type t_terminates = identified_predicate option
(** Type of a function that, given a {!Kernel_function.t} and a
- {!Cil_types.spec}, returns a clause. Accepted clause types include
+ {!type:Cil_types.spec}, returns a clause. Accepted clause types include
{!t_exits}, {!t_assigns}, {!t_requires}, {!t_allocates} and {!t_terminates}.
*)
type 'a gen = (kernel_function -> spec -> 'a)
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index b91a7413f85d67bf6563cf87ad3e5f3629c05fb3..7981195c73d97c66926034828e477dd2ba70319d 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -591,7 +591,7 @@ and typeinfo = {
{!Cil_types.varinfo} structure. A global {!Cil_types.varinfo} can be
introduced with the [GVarDecl] or [GVar], [GFunDecl] or [GFun] globals.
A local varinfo can be introduced as part of a function definition
- {!Cil_types.fundec}.
+ {!type:Cil_types.fundec}.
All references to a given global or local variable must refer to the same
copy of the [varinfo]. Each [varinfo] has a globally unique identifier that
@@ -925,8 +925,8 @@ and offset =
(** A special kind of expressions are those that can appear as initializers for
global variables (initialization of local variables is turned into
assignments). The initializers are represented as type
- {!Cil_types.init}. You can create initializers with {!Cil.makeZeroInit} and
- you can conveniently scan compound initializers them with
+ {!type:Cil_types.init}. You can create initializers with {!Cil.makeZeroInit}
+ and you can conveniently scan compound initializers them with
{!Cil.foldLeftCompound}. *)
(** Initializers for global variables. *)
@@ -974,10 +974,10 @@ and local_init =
(** A function definition is always introduced with a [GFun] constructor at the
top level. All the information about the function is stored into a
- {!Cil_types.fundec}. Some of the information (e.g. its name, type, storage,
- attributes) is stored as a {!Cil_types.varinfo} that is a field of the
- [fundec]. To refer to the function from the expression language you must use
- the [varinfo].
+ {!type:Cil_types.fundec}. Some of the information (e.g. its name, type,
+ storage, attributes) is stored as a {!Cil_types.varinfo} that is a field of
+ the [fundec]. To refer to the function from the expression language you must
+ use the [varinfo].
The function definition contains, in addition to the body, a list of all the
local variables and separately a list of the formals. Both kind of variables
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 09e942da7aee0bdadbb192f1e0ea454d2af89281..599e2c668e1cd4e3e64e18139a688ea8f690e346 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -646,18 +646,19 @@ type combineFunction =
@raise Cannot_combine with an explanation when the type cannot be combined.
@since 28.0-Nickel
- @before 29.0-Copper [strictInteger (true)] and [strictReturnTypes (false)]
- were optional
+ @before 29.0-Copper [strictInteger:true] and [strictReturnTypes:false] were
+ optional
*)
val combineTypesGen : ?emitwith:(Log.event -> unit) -> combineFunction ->
strictInteger:bool -> strictReturnTypes:bool ->
combineWhat -> typ -> typ -> typ
-(** Specialized version of {!combineTypesGen], we suppose here that if two
- global symbols are equal, then they are the same object.
+(** Specialized version of {!combineTypesGen}, we suppose here that if two
+ global symbols are equal, then they are the same object. [strictInteger] is
+ [true] by default, [strictReturnTypes] is [false] by default.
@since 28.0-Nickel
- @before 29.0-Copper [strictInteger (true)] was not present and left with its
+ @before 29.0-Copper [strictInteger] was not present and left with its
default value in combineTypesGen.
*)
val combineTypes : ?strictInteger:bool -> ?strictReturnTypes:bool ->
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index 764389f33112a38ad2c02cc00a4bbd3bf518d1fe..d98cb0aaf756fec352ee1f6f7045dda8d2316c98 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -41,7 +41,8 @@ val is_extension: plugin:string -> string -> bool
val is_extension_block: plugin:string -> string -> bool
(** Return [true] if a module importer is registered for the given name and
- plugin. @since 30.0-Zinc
+ plugin.
+ @since 30.0-Zinc
*)
val is_importer: plugin:string -> string -> bool
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 72feb75538e116e6e49c99f53d5d66215789f75e..e7ac47576eb48cb79c858d48ce9cad2266ecf88c 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -336,7 +336,7 @@ type behavior = {
}
(** Function or statement contract. This type shares the name of its
- constructors with {!Cil_types.spec}. *)
+ constructors with {!type:Cil_types.spec}. *)
type spec = {
mutable spec_behavior : behavior list;
(** behaviors *)
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 090b626507e2f50f7951b436ff757701f95457a6..c063b0fa6d5f16c814946597fd18e63331e108c5 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -162,7 +162,7 @@ end
end] *)
module Undefined: Undefined
-(** Same as {!Undefined}, but the type is supposed to be marshallable by the
+(** Same as {!module:Undefined}, but the type is supposed to be marshallable by the
standard OCaml way (in particular, no hash-consing or projects inside
the type).
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
@@ -354,7 +354,7 @@ val filepath: Filepath.t Type.t
(** {2 Generic functors for polymorphic types} *)
(* ****************************************************************************)
-(** Output signature of {!Polymorphic}. *)
+(** Output signature of {!module:Polymorphic}. *)
module type Polymorphic = sig
include Type.Polymorphic
module Make(T: S) : S with type t = T.t poly
@@ -382,7 +382,7 @@ module Polymorphic
end) :
Polymorphic with type 'a poly = 'a P.t
-(** Output signature of {!Polymorphic2}. *)
+(** Output signature of {!module:Polymorphic2}. *)
module type Polymorphic2 = sig
include Type.Polymorphic2
module Make(T1: S)(T2: S) : S with type t = (T1.t, T2.t) poly
@@ -414,7 +414,7 @@ module Polymorphic2
end) :
Polymorphic2 with type ('a, 'b) poly = ('a, 'b) P.t
-(** Output signature of {!Polymorphic3}.
+(** Output signature of {!module:Polymorphic3}.
@since Oxygen-20120901 *)
module type Polymorphic3 = sig
include Type.Polymorphic3
@@ -454,7 +454,7 @@ module Polymorphic3
end) :
Polymorphic3 with type ('a, 'b, 'c) poly = ('a, 'b, 'c) P.t
-(** Output signature of {!Polymorphic4}.
+(** Output signature of {!module:Polymorphic4}.
@since Oxygen-20120901 *)
module type Polymorphic4 = sig
include Type.Polymorphic4
diff --git a/src/libraries/datatype/structural_descr.mli b/src/libraries/datatype/structural_descr.mli
index b44c179432be95817fcdbf8c585e214736735cf3..f108f98e1c18645724404de3be7ea5f1462d8311 100644
--- a/src/libraries/datatype/structural_descr.mli
+++ b/src/libraries/datatype/structural_descr.mli
@@ -29,7 +29,7 @@
(* ********************************************************************** *)
(** Type used for handling (possibly mutually) recursive structural
- descriptors. See module {!Recursive}. *)
+ descriptors. See module {!module:Recursive}. *)
type recursive
type single_pack = private Unmarshal.t
@@ -39,7 +39,7 @@ type pack = private
| Nopack (** Was impossible to build a pack. *)
| Pack of single_pack (** A standard pack. *)
| Recursive of recursive (** Pack for a recursive descriptor.
- See module {!Recursive}. *)
+ See module {!module:Recursive}. *)
(** Type of internal representations of OCaml type.
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 195b3cb745ecc82c383b1ece1937141bd8d92b36..cc2bd56a2cf27c09c04c1dc2256c602a4871ddd3 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -213,7 +213,8 @@ module type Polymorphic2_input = sig
val reprs: 'a -> 'b -> ('a, 'b) t list
end
-(** Same as {!Polymorphic} for polymorphic types with two type variables. *)
+(** Same as {!module:Polymorphic} for polymorphic types with two type
+ variables. *)
module type Polymorphic2 = sig
type ('a, 'b) poly
val instantiate: 'a t -> 'b t -> ('a, 'b) poly t * bool
@@ -225,8 +226,8 @@ end
module Polymorphic2(T:Polymorphic2_input)
: Polymorphic2 with type ('a, 'b) poly = ('a, 'b) T.t
-(** Instance of {!Polymorphic2} for functions: same signature than
- {!Polymorphic2} with possibility to specify a label for the function
+(** Instance of {!module:Polymorphic2} for functions: same signature than
+ {!module:Polymorphic2} with possibility to specify a label for the function
parameter. *)
module Function : sig
type ('a, 'b) poly = 'a -> 'b
@@ -255,7 +256,8 @@ module type Polymorphic3_input = sig
val reprs: 'a -> 'b -> 'c -> ('a, 'b, 'c) t list
end
-(** Same as {!Polymorphic} for polymorphic types with three type variables.
+(** Same as {!module:Polymorphic} for polymorphic types with three type
+ variables.
@since Oxygen-20120901 *)
module type Polymorphic3 = sig
type ('a, 'b, 'c) poly
@@ -283,7 +285,8 @@ module type Polymorphic4_input = sig
val reprs: 'a -> 'b -> 'c -> 'd -> ('a, 'b, 'c, 'd) t list
end
-(** Same as {!Polymorphic} for polymorphic types with four type variables.
+(** Same as {!module:Polymorphic} for polymorphic types with four type
+ variables.
@since Oxygen-20120901 *)
module type Polymorphic4 = sig
type ('a, 'b, 'c, 'd) poly
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index 237fea9db76725b41c065407ed8599d4c350b414..c027663e6d84b9295e53c4db1f5ea97d03b4d7f4 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -100,7 +100,7 @@ val get_name: t -> string
(** Project name. Two projects may have the same name. *)
val get_unique_name: t -> string
-(** @return a project name based on {!name} but different of each others
+(** @return a project name based on {!field:name} but different of each others
[unique_name]. *)
val set_name: t -> string -> unit
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index fc1e99f49e583682a4718d2c16c6af6dbf231963..f316ad1bdc734bdf4bbf0b31dbff9c92c490224d 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -253,10 +253,10 @@ val mkdir : ?parents:bool -> Filepath.Normalized.t -> Unix.file_perm -> bool
in a modified state before raising an exception.
Returns [true] if the directory was created, [false] otherwise.
@raise Unix.Unix_error if cannot create [name] or its parents.
+ @raise Failure if the path exists but is not a directory
@since 19.0-Potassium
- @since 28.0-Nickel added check for existence of path (error if exists
- but not a directory, otherwise do nothing if directory already exists).
- Changed type of [name] argument and return type.
+ @before 28.0-Nickel [name] argument was of type [string] and the returned
+ type was [unit]. Also, the function did not check for path's existence.
*)
val safe_at_exit : (unit -> unit) -> unit
diff --git a/src/libraries/utils/bitvector.mli b/src/libraries/utils/bitvector.mli
index 2cccaa9bd9c37156c302128c9244f9b78abf84b1..e74f16b2d0ce18d45e459eefc0a46e7c6a281f63 100644
--- a/src/libraries/utils/bitvector.mli
+++ b/src/libraries/utils/bitvector.mli
@@ -64,7 +64,7 @@ val bor: int -> t -> t -> t
val bxor: int -> t -> t -> t (* bitwise difference *)
val beq: int -> t -> t -> t (* bitwise equivalence/equality *)
-(** {2 Generic Bitwise Operations}. *)
+(** {2 Generic Bitwise Operations} *)
(** Prefer using these rather than create intermediary bitvectors. *)
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index c169cbe4fd9b75ce7866e219d4f9885c59df0ecf..6997982f19995962372084a2ff7ad7d66f450564 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -195,7 +195,7 @@ val pp_items :
(default is [Format.pp_print_string])
- [~pp_item] pretty-printer to print each element.
- There is also a low-level API to this feature, provided by {!marger},
+ There is also a low-level API to this feature, provided by {!val:marger},
{!pp_margin} and {!add_margin} below.
*)
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index 5ced2f360197420c89747d3266da0bde6547ce5b..72c37d29fefc96a40e2a2cb74c6319973affc959 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -128,13 +128,16 @@ val exp : map -> exp -> node option
For optimized access, all the fonctions in this section return
unnormalized nodes and may raise [Not_found] for not localized routes. *)
-(** Unormalized. @raises Not_found *)
+(** Unormalized.
+ @raises Not_found *)
val cvar : map -> varinfo -> node
-(** Unormalized. @raises Not_found *)
+(** Unormalized.
+ @raises Not_found *)
val field : map -> node -> fieldinfo -> node
-(** Unormalized. @raises Not_found *)
+(** Unormalized.
+ @raises Not_found *)
val index : map -> node -> typ -> node
(** Normalized list of leaf nodes. *)