diff --git a/src/kernel_internals/parsing/logic_preprocess.mli b/src/kernel_internals/parsing/logic_preprocess.mli
index 90a5a8540ed25d2c1f4556fec87271f8206374bb..38fecb6f34f5464baef321fa7bdf0ff974a57289 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mli
+++ b/src/kernel_internals/parsing/logic_preprocess.mli
@@ -33,9 +33,6 @@
(gcc pre-processing differs between .c and .cxx files)
@raises Sys_error if the file cannot be opened.
-
- @modifies Oxygen-20120901: added suffix argument
-
*)
val file: string -> (string -> string -> string) -> string ->
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/abstract_interp/lattice_type.mli b/src/kernel_services/abstract_interp/lattice_type.mli
index 7ac4e1bf59ab43a80a9a8a6a3a01940e6b7ea085..f5e0608d520c6c801358ff9a8c9a478e7cc45036 100644
--- a/src/kernel_services/abstract_interp/lattice_type.mli
+++ b/src/kernel_services/abstract_interp/lattice_type.mli
@@ -73,7 +73,7 @@ end
Conversely, some functions, suffixed by [_under] assumes that their arguments
are under-approximations, and returns a result that under-approximates the
concrete operation. The functions [link] and [meet] in
- {With_Under_Approximation} are exceptions, that are not suffixed by [_under].
+ {!With_Under_Approximation} are exceptions, that are not suffixed by [_under].
Finally, some functions are *exact*, in the sense that they preserve the
concretization of the concrete function. Hence, they implement
@@ -165,7 +165,7 @@ module type Full_AI_Lattice_with_cardinality = sig
end
-(** {2 Results of generic functors, in module {!Abstract_interp}. } *)
+(** {2 Results of generic functors, in module [Abstract_interp]. } *)
(** Generic signature for the base elements of a lattice *)
module type Lattice_Value = Datatype.S_with_collections
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..5e3bd30bf63a7d4ea8fe48c20011d4c9c2616778 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -340,9 +340,7 @@ and attrparam =
one and use {!Cil.copyCompInfo} to copy one (this ensures that a new key is
assigned and that the fields have the right pointers to parents.).
@plugin development guide
-
- @since 23.0-Vanadium [cfields] is an option, [None] is used for incomplete
- types (in replacement of removed field [cdefined]) *)
+*)
and compinfo = {
mutable cstruct: bool;
(** [true] if struct, [false] if union *)
@@ -365,7 +363,10 @@ and compinfo = {
back to the host compinfo. This means that you should not share
fieldinfo's between two compinfo's.
- None value means that the type is incomplete. *)
+ None value means that the type is incomplete.
+
+ @before 23.0-Vanadium this field was not optional
+ *)
mutable cattr: attributes;
(** The attributes that are defined at the same time as the composite
@@ -787,7 +788,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 +823,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
@@ -1391,7 +1393,7 @@ and term_node =
| Tinter of term list (** intersection of terms. *)
| Tcomprehension of
term * quantifiers * predicate option
- (** set defined in comprehension ({t \{ t[i] | integer i; 0 <= i < 5\}}) *)
+ (** set defined in comprehension ([{ t[i] | integer i; 0 <= i < 5}]) *)
| Trange of term option * term option (** range of integers. *)
| Tlet of logic_info * term (** local binding *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 5e1be0e3bc823de0d48cbd0bc8ffaf20230bff12..0c954057a436afbac342fdb608cfb937cf405271 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -67,7 +67,7 @@ val find_all_labels: t -> Datatype.String.Set.t
val clear_sid_info: unit -> unit
(** removes any information related to statements in kernel functions.
- ({i.e.} the table used by the function below).
+ (i.e. the table used by the function below).
- Must be called when the Ast has silently changed
(e.g. with an in-place visitor) before calling one of
the functions below
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 16f4828980bb0c648de24f4539b7978aa5735cfb..d45b91734daebbe69d4e15629b11c5587c0a25a1 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1065,210 +1065,6 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string io_name
pp_other_loc io_loc
-(* -------------------------------------------------------------------------- *)
-(* --- Legacy Property Names --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Shall be deprecated *)
-module LegacyNames =
-struct
-
- module NamesTbl =
- State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
- (struct
- let name = "PropertyNames"
- let dependencies = [ ]
- let size = 97
- end)
- module IndexTbl =
- State_builder.Hashtbl(Hashtbl)(Datatype.String)
- (struct
- let name = "PropertyIndex"
- let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
- let size = 97
- end)
-
- let self = IndexTbl.self
-
- let kf_prefix kf = (Ast_info.Function.get_vi kf.fundec).vname ^ "_"
-
- let ident_names names =
- List.filter (function "" -> true
- | _ as n -> '\"' <> (String.get n 0) ) names
-
- let pp_names fmt l =
- let l = ident_names l in
- match l with [] -> ()
- | _ -> Format.fprintf fmt "_%a"
- (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
-
- let pp_code_annot_names fmt ca =
- match ca.annot_content with
- | AAssert(for_bhv,pred) | AInvariant(for_bhv,_,pred) ->
- let named_pred = pred.tp_statement in
- let pp_for_bhv fmt l =
- match l with
- | [] -> ()
- | _ -> Format.fprintf fmt "_for_%a"
- (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
- in
- Format.fprintf fmt "%a%a" pp_names named_pred.pred_name pp_for_bhv for_bhv
- | AVariant(term, _) -> pp_names fmt term.term_name
- | _ -> () (* TODO : add some more names ? *)
-
- let behavior_prefix b =
- if Cil.is_default_behavior b then ""
- else b.b_name ^ "_"
-
- let variant_suffix = function
- | (_,Some s) -> s.l_var_info.lv_name
- | _ -> ""
-
- let string_of_termination_kind = function
- Normal -> "post"
- | Exits -> "exit"
- | Breaks -> "break"
- | Continues -> "continue"
- | Returns -> "return"
-
- let stmt_prefix _s = "stmt_"
-
- let ki_prefix = function Kglobal -> "" | Kstmt s -> stmt_prefix s
-
- let extended_loc_prefix = function
- | ELContract kf -> kf_prefix kf
- | ELStmt (kf,s) -> kf_prefix kf ^ stmt_prefix s
- | ELGlob -> "global_"
-
- let other_loc_prefix = function
- | OLContract kf -> kf_prefix kf
- | OLStmt (kf,s) -> kf_prefix kf ^ stmt_prefix s
- | OLGlob _ -> "global_"
-
- let predicate_kind_txt pk ki =
- let name = match pk with
- | PKRequires b -> (behavior_prefix b) ^ "pre"
- | PKAssumes b -> (behavior_prefix b) ^ "assume"
- | PKEnsures (b, tk) -> (behavior_prefix b) ^ string_of_termination_kind tk
- | PKTerminates -> "term"
- in
- (ki_prefix ki) ^ name
-
- let active_prefix fmt a =
- let print_one a = Format.fprintf fmt "_%s" a in
- Datatype.String.Set.iter print_one a
-
- let rec id_prop_txt p = match p with
- | IPPredicate {ip_kind=pk;ip_kf=kf;ip_kinstr=ki;ip_pred=idp} ->
- Format.asprintf "%s%s%a"
- (kf_prefix kf) (predicate_kind_txt pk ki)
- pp_names (Logic_const.pred_of_id_pred idp).pred_name
- | IPExtended {ie_ext={ext_name};ie_loc=le} ->
- Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [ext_name]
- | IPCodeAnnot {ica_kf=kf; ica_ca=ca} ->
- let name = match ca.annot_content with
- | AAssert (_, {tp_kind}) -> Cil_printer.string_of_assert tp_kind
- | AInvariant (_,loop,{tp_kind}) ->
- let kw = if loop then "invariant" else "loop_invariant" in
- Cil_printer.ident_of_predicate ~kw tp_kind
- | APragma _ -> "pragma"
- | AStmtSpec _ -> "contract"
- | AAssigns _ -> "assigns"
- | AVariant _ -> "variant"
- | AAllocation _ -> "allocates"
- | AExtended(_,_,{ext_name}) -> ext_name
- in Format.asprintf "%s%s%a" (kf_prefix kf) name pp_code_annot_names ca
- | IPComplete {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
- let lb = Datatype.String.Set.elements lb in
- Format.asprintf "%s%s%acomplete%a"
- (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
- | IPDisjoint {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
- let lb = Datatype.String.Set.elements lb in
- Format.asprintf "%s%s%adisjoint%a"
- (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
- | IPDecrease {id_kf=kf; id_ca=None; id_variant=variant} ->
- (kf_prefix kf) ^ "decr" ^ (variant_suffix variant)
- | IPDecrease {id_kf=kf; id_variant=variant} ->
- (kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
- | IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
- | IPLemma {il_name=name; il_pred} ->
- Format.asprintf "%s_%s%a"
- (Cil_printer.ident_of_lemma il_pred.tp_kind)
- name pp_names il_pred.tp_statement.pred_name
- | IPTypeInvariant {iti_name; iti_pred} ->
- Format.asprintf "type_invariant_%s%a"
- iti_name pp_names iti_pred.pred_name
- | IPGlobalInvariant {igi_name; igi_pred} ->
- Format.asprintf "global_invariant_%s%a"
- igi_name pp_names igi_pred.pred_name
- | IPAllocation {ial_kf=kf; ial_kinstr=ki; ial_bhv=Id_contract (a,b)} ->
- Format.asprintf "%s%s%a%sallocates"
- (kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
- | IPAllocation {ial_kf=kf; ial_kinstr=Kstmt _; ial_bhv=Id_loop ca} ->
- Format.asprintf "%sloop_allocates%a"
- (kf_prefix kf) pp_code_annot_names ca
- | IPAllocation _ -> assert false
- | IPAssigns {ias_kf=kf; ias_kinstr=ki; ias_bhv=Id_contract (a,b)} ->
- Format.asprintf "%s%s%a%sassign"
- (kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
- | IPAssigns {ias_kf=kf; ias_kinstr=Kstmt _; ias_bhv=Id_loop ca} ->
- Format.asprintf "%sloop_assign%a"
- (kf_prefix kf) pp_code_annot_names ca
- | IPAssigns _ -> assert false
- | IPFrom {if_from=(out,_)} ->
- "from_id_"^(string_of_int (out.it_id))
- | IPReachable _ -> "reachable_stmt"
- | IPBehavior {ib_kf=kf; ib_kinstr=ki; ib_active=a; ib_bhv=b} ->
- Format.asprintf "%s%s%a%s"
- (kf_prefix kf) (ki_prefix ki) active_prefix a b.b_name
- | IPPropertyInstance {ii_kf=kf; ii_stmt=stmt; ii_ip=ip} ->
- Format.asprintf "specialization_%s_at_%t" (id_prop_txt ip)
- (fun fmt ->
- Format.fprintf fmt "%a_stmt_%d" Kernel_function.pretty kf stmt.sid)
- | IPOther {io_name; io_loc} -> other_loc_prefix io_loc ^ io_name
-
- (** function used to normalize basename *)
- let normalize_basename s =
- let is_valid_char_id = function
- | 'a'..'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> true
- | _ -> false
- and is_numeric = function
- | '0'..'9' -> true
- | _ -> false
- in
- if s ="" then "property"
- else
- let s = String.map (fun c -> if not (is_valid_char_id c) then '_' else c) s in
- if is_numeric s.[0] then "property_" ^ s else s
-
- (** returns the name that should be returned by the function [get_prop_name_id] if the given property has [name] as basename. That name is reserved so that [get_prop_name_id prop] can never return an identical name. *)
- let reserve_name_id basename =
- let basename = normalize_basename basename in
- try
- let speed_up_start = NamesTbl.find basename in
- (* this basename is already reserved *)
- let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ;
- basename
-
- (** returns the basename of the property. *)
- let get_prop_basename ip = normalize_basename (id_prop_txt ip)
-
- (** returns a unique name identifying the property.
- This name is built from the basename of the property. *)
- let get_prop_name_id ip =
- try IndexTbl.find ip
- with Not_found -> (* first time we are asking for a name for that [ip] *)
- let basename = get_prop_basename ip in
- let unique_name = reserve_name_id basename in
- IndexTbl.add ip unique_name ;
- unique_name
-
-end
-
(* -------------------------------------------------------------------------- *)
(* --- Property Names --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 6d9f38b4c4eb2f6c042f597bdbeeab29ebbf9a24..eaf6c8bc0db251ebc066d74efacee36d742d1a6b 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -519,16 +519,6 @@ val source: identified_property -> Filepath.position option
(** {2 names} *)
(**************************************************************************)
-
-(** @since 19.0-Potassium deprecated old naming scheme,
- to be removed in future versions. *)
-module LegacyNames :
-sig
- val self: State.t
- val get_prop_basename: identified_property -> string
- val get_prop_name_id: identified_property -> string
-end
-
(** @since Oxygen-20120901 *)
module Names :
sig
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 1ac60ebf9d079e57ad8f043c645738861fc38da5..3252bc6eaf56fda2255248801eb65f64cddcf8ca 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -41,14 +41,15 @@
entry point to [s]. It also depends on an explicit set of hypotheses [H]
indicating when emitting the property (see function {!emit}). *)
type emitted_status =
- | True (** for each execution path [ep] from the program entry point to [s],
- the formula (/\_{h in H} h) ==> P(ep) is true *)
- | False_if_reachable (** for each execution path [ep] from the program entry
- point to [s], the formula (/\_{h in H} h) ==> P(ep)
- is false *)
- | False_and_reachable (** it exists an execution path [ep] from the program
- entry point to [s] such that the formula (/\_{h in
- H} h) ==> P(ep) is false *)
+ | True
+ (** for each execution path [ep] from the program entry point to [s],
+ the formula [(/\_{h in H} h) ==> P(ep)] is true *)
+ | False_if_reachable
+ (** for each execution path [ep] from the program entry point to [s],
+ the formula [(/\_{h in H} h) ==> P(ep)] is false *)
+ | False_and_reachable
+ (** it exists an execution path [ep] from the program entry point to [s]
+ such that the formula [(/\_{h in H} h) ==> P(ep)] is false *)
| Dont_know (** any other case *)
module Emitted_status: Datatype.S with type t = emitted_status
@@ -68,7 +69,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/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 22f3a198087e98cce8c0f63009ad7da9638a5d04..a651c98bf1f72df4f4ded14dda5d38bdcfaca299 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -93,7 +93,6 @@ type extension_printer =
p)])
| [] -> let id = !count in incr count; Ext_id id
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
-
let () = Acsl_extension.register_behavior "FOO" foo_typer false
]
@plugin development guide
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index df6e83336874b7a7fd735a30a60fbf3bb0c214ff..0aa8ba37d6d88ca10c3049d78c8bdb8804905aac 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -86,7 +86,7 @@ val behavior_precondition : goal:bool -> funbehavior -> predicate
val behavior_postcondition :
goal:bool -> funbehavior -> termination_kind -> predicate
(** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
- For flag [~goal] see {Ast_info.precondition} above.
+ For flag [~goal] see {!Ast_info.precondition} above.
@before 23.0-Vanadium no [goal] flag.
*)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 9c4c6ca29ca0f8e6119ce1cebd5fdc0a5e367c09..5e1397685e6239e0cca7c3a30ecf880ba7039462 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -591,8 +591,8 @@ val isVariadicListType: typ -> bool
val argsToList:
(string * typ * attributes) list option -> (string * typ * attributes) list
-(** @since 20.0-Calcium
- Obtain the argument lists (non-ghost, ghosts) ([], [] if None) *)
+(** Obtain the argument lists (non-ghost, ghosts) ([], [] if None)
+ @since 20.0-Calcium *)
val argsToPairOfLists:
(string * typ * attributes) list option ->
(string * typ * attributes) list * (string * typ * attributes) list
@@ -1526,10 +1526,12 @@ val mk_behavior :
?extended:acsl_extension list ->
unit ->
Cil_types.behavior
-(** @since Carbon-20101201
- returns a dummy behavior with the default name [Cil.default_behavior_name].
+(** returns a dummy behavior with the default name [Cil.default_behavior_name].
invariant: [b_assumes] must always be
- empty for behavior named [Cil.default_behavior_name] *)
+ empty for behavior named [Cil.default_behavior_name]
+
+ @since Carbon-20101201
+*)
val default_behavior_name: string
(** @since Carbon-20101201 *)
@@ -2041,7 +2043,9 @@ val is_empty_funspec: funspec -> bool
val is_empty_behavior: funbehavior -> bool
(* ************************************************************************* *)
-(** {2 ALPHA conversion} has been moved to the Alpha module. *)
+(** {2 Renaming} *)
+
+(** See also the {!Alpha} module for other renaming operations. *)
(* ************************************************************************* *)
(** 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/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 079f6b4965744b235d14b2573614777c369deb01..2a7d97c98f428e97ff7f5cbba534aa74270a7f91 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -252,7 +252,7 @@ val is_set_type: logic_type -> bool
(** [set_conversion ty1 ty2] returns a set type as soon as [ty1] and/or [ty2]
is a set. Elements have type [ty1], or the type of the elements of [ty1] if
- it is itself a set-type ({i.e.} we do not build set of sets that way).
+ it is itself a set-type (i.e. we do not build set of sets that way).
*)
val set_conversion: logic_type -> logic_type -> logic_type
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index 572ee38ca0221df19644f0e79d27e961e1b6d87e..b30852478e34e2fdafdaeb776ec461b80a1a478c 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -309,7 +309,7 @@ val add_aliases:
option name [orig].
If [visible] is set to false, the aliases do not appear in help messages.
If [deprecated] is set to true, the use of the aliases emits a warning.
- @Invalid_argument if an alias name is the empty string
+ @raise Invalid_argument if an alias name is the empty string
@since Carbon-20110201
@before 22.0-Titanium no [visible] and [deprecated] arguments. *)
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 545f1cc5147c6b1775d3ebe31e3704ee5312346c..85d47d3a0901577bd83b3853d7cfe94fcb5ec3a9 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -97,8 +97,8 @@ and lexpr_node =
| PLconstant of constant (** a constant. *)
| PLunop of unop * lexpr (** unary operator. *)
| PLbinop of lexpr * binop * lexpr (** binary operator. *)
- | PLdot of lexpr * string (** field access ({t a.x}) *)
- | PLarrow of lexpr * string (** field access ({t a->x})*)
+ | PLdot of lexpr * string (** field access ([a.x]) *)
+ | PLarrow of lexpr * string (** field access ([a->x])*)
| PLarrget of lexpr * lexpr (** array access. *)
| PLold of lexpr (** expression refers to pre-state of a function. *)
| PLat of lexpr * string (** expression refers to a given program point. *)
@@ -148,7 +148,7 @@ and lexpr_node =
(* tsets *)
| PLcomprehension of lexpr * quantifiers * lexpr option
(** set of expression defined in comprehension
- ({t \{ e | integer i; P(i)\}})*)
+ ([{ e | integer i; P(i)}])*)
| PLset of lexpr list
(** sets of elements. *)
| PLunion of lexpr list
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index b2a2b5289f63e294a7aed91fb6c023545f0609f7..a44b6b4ae22032c9aedd987c3bf90d05d71c1e68 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -61,9 +61,9 @@ type ('a,'b) pretty_aborter =
?current:bool -> ?source:Filepath.position -> ?echo:bool ->
?append:(Format.formatter -> unit) ->
('a,formatter,unit,'b) format4 -> 'a
-(** @since Beryllium-20090601-beta1
- Same as {!Log.pretty_printer} except that channels having this type
+(** Same as {!Log.pretty_printer} except that channels having this type
denote a fatal error aborting Frama-C.
+ @since Beryllium-20090601-beta1
*)
(* -------------------------------------------------------------------------- *)
@@ -87,7 +87,7 @@ exception FeatureRequest of Filepath.position option * string * string
You may catch [FeatureRequest(s,p,r)] to support degenerated behavior.
The (optional) source location is s, the responsible plugin is 'p'
and the feature request is 'r'.
- @modified 23.0-Vanadium added source location.
+ @before 23.0-Vanadium there was no source location
*)
(* -------------------------------------------------------------------------- *)
@@ -210,7 +210,7 @@ module type Messages = sig
If the exception is not caught, Frama-C displays a feature-request
message to the user.
@since Beryllium-20090901
- @modified 23.0-Vanadium added current and source arguments.
+ @before 23.0-Vanadium there was no [current] and [source] arguments.
*)
val deprecated: string -> now:string -> ('a -> 'b) -> ('a -> 'b)
@@ -223,22 +223,22 @@ module type Messages = sig
val with_result : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_result f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified 18.0-Argon the argument of the continuation is optionnal *)
+ *)
val with_warning : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_warning f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified 18.0-Argon the argument of the continuation is optionnal *)
+ *)
val with_error : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_error f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified 18.0-Argon the argument of the continuation is optionnal *)
+ *)
val with_failure : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_failure f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified 18.0-Argon the argument of the continuation is optionnal *)
+ *)
val log : ?kind:kind -> ?verbose:int -> ?debug:int -> 'a pretty_printer
(** Generic log routine. The default kind is [Result]. Use cases (with
@@ -480,7 +480,7 @@ val print_delayed : (Format.formatter -> unit) -> unit
val set_current_source : (unit -> Filepath.position) -> unit
(* Forward reference to the function returning the current location,
used when [~current:true] is set on printers. Currently set
- in {Cil}. Not for the casual user. *)
+ in {!Cil}. Not for the casual user. *)
val check_not_yet: (event -> bool) ref
(* Checks whether a message been emitted already, in which case it is
diff --git a/src/libraries/datatype/descr.mli b/src/libraries/datatype/descr.mli
index 7a03c2a3417fcd28076a5c602eefbaf7c352508a..f55a48f9b835838debbbcae414b104d2e414da5e 100644
--- a/src/libraries/datatype/descr.mli
+++ b/src/libraries/datatype/descr.mli
@@ -107,7 +107,7 @@ val of_structural: 'a Type.t -> Structural_descr.t -> 'a t
ensures safety.
@since Carbon-20101201 *)
-(** {3 Builders mapping {!Unmarshal}'s transformers} *)
+(** {3 Builders mapping [Unmarshal]'s transformers} *)
val dependent_pair: 'a t -> ('a -> 'b t) -> ('a * 'b) t
(** Similar to {!Unmarshal.Dependent_pair}, but safe.
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index 15b0fe12ff2369fe4cfc40107615e50341db6023..c3a630b794a3869907eeaf8819e7a541622ae9f3 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -236,7 +236,7 @@ module type Weak_hashtbl = sig
val find: data -> data
(** [find x] returns an instance of [x] found in table.
- @Raise Not_found if there is no such element.
+ @raise Not_found if there is no such element.
@since Boron-20100401 *)
val find_all: data -> data list
@@ -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..50664e713e87bfb30dd7cd09267a89b196fd3e77 100644
--- a/src/libraries/utils/bitvector.mli
+++ b/src/libraries/utils/bitvector.mli
@@ -54,8 +54,9 @@ val equal: t -> t -> bool
val compare: t -> t -> int
val hash: t -> int
-(** {2 Bitwise Binary Operations}
- The first argument is the size of the vectors. *)
+(** {2 Bitwise Binary Operations} *)
+
+(** The first argument is the size of the vectors. *)
val bnot: int -> t -> t
val band: int -> t -> t -> t
@@ -63,8 +64,9 @@ 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}.
- Prefer using these rather than create intermediary bitvectors. *)
+(** {2 Generic Bitwise Operations}. *)
+
+(** Prefer using these rather than create intermediary bitvectors. *)
val bitwise_op2: int -> (int -> int -> int) -> t -> t -> t
val bitwise_op3: int -> (int -> int -> int -> int) -> t -> t -> t -> t
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 7863d6e262e83a8fdd1feff875263fdf6b727809..ac22f67cbcf9734c2c2764b87b0d536a517b3ba5 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -80,7 +80,7 @@ val full_command :
-> stdout:Unix.file_descr
-> stderr:Unix.file_descr
-> Unix.process_status
-(** Same arguments as {Unix.create_process} but returns only when
+(** Same arguments as {!Unix.create_process} but returns only when
execution is complete.
@raise Sys_error when a system error occurs *)
@@ -96,7 +96,7 @@ val full_command_async :
-> stdout:Unix.file_descr
-> stderr:Unix.file_descr
-> (unit -> process_result)
-(** Same arguments as {Unix.create_process}.
+(** Same arguments as {!Unix.create_process}.
@return a function to call to check if the process execution
is complete.
You must call this function until it returns a Result
@@ -108,7 +108,7 @@ val command_async :
?stderr:Buffer.t ->
string -> string array
-> (unit -> process_result)
-(** Same arguments as {Unix.create_process}.
+(** Same arguments as {!Unix.create_process}.
@return a function to call to check if the process execution
is complete.
You must call this function until it returns a Result
@@ -123,7 +123,7 @@ val command :
?stderr:Buffer.t ->
string -> string array
-> Unix.process_status
-(** Same arguments as {Unix.create_process}.
+(** Same arguments as {!Unix.create_process}.
When this function returns, the stdout and stderr of the child
process will be filled into the arguments buffer.
@raise Sys_error when a system error occurs
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index ba4179ae57c7f7e8cdfea47694125949ee2bf92e..c203bb97be8e812d4e66344dc3b4a551f3b605a7 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -66,7 +66,9 @@ val of_list : t list -> t
val of_array : t array -> t
val of_fields : (string * t) list -> t
-(** {2 Parsers} Parsing raise [Error] in case of error. *)
+(** {2 Parsers} *)
+
+(** Parsing raise [Error] in case of error. *)
val load_lexbuf : Lexing.lexbuf -> t
(** Consumes the entire buffer. *)
@@ -80,7 +82,9 @@ val load_string : string -> t
val load_file : string -> t
(** May also raise system exception. *)
-(** {2 Printers} Printers use formatting unless [~pretty:false]. *)
+(** {2 Printers} *)
+
+(** Printers use formatting unless [~pretty:false]. *)
val save_string : ?pretty:bool -> t -> string
val save_buffer : ?pretty:bool -> Buffer.t -> t -> unit
@@ -88,9 +92,9 @@ val save_channel : ?pretty:bool -> out_channel -> t -> unit
val save_formatter : ?pretty:bool -> Format.formatter -> t -> unit
val save_file : ?pretty:bool -> string -> t -> unit
-(** {2 Accessors}
- Accessors raise exception [Invalid_argument] in case of wrong
- format. *)
+(** {2 Accessors} *)
+
+(** Accessors raise exception [Invalid_argument] in case of wrong format. *)
val bool : t -> bool
(** Extract [True] and [False] only.
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 0b91ab6a295cf8ffe3e6abe5c739a73d04845372..c65f3cc8dcb357ab351b70b97d5b8f0bd2ea2f6f 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -72,7 +72,7 @@ val gmpz: number_ty
val rational: number_ty
val nan: number_ty
-(** {3 Useful operations over {!number_ty}} *)
+(** {3 Useful operations over [number_ty]} *)
exception Not_a_number
val typ_of_number_ty: number_ty -> typ
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/gui/design.mli b/src/plugins/gui/design.mli
index e833a41927ad1ad20372d8e3bd8e03ef4ad81347..f920b516f972b307c8ec3a04529c79c0d8dceb6a 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -190,11 +190,12 @@ class type main_window_extension_points = object
updated. *)
method redisplay : unit -> unit
- (** @since Nitrogen-20111001
- Force to redisplay the current displayed buffer.
+ (** Force to redisplay the current displayed buffer.
Plugins should call this method whenever they have changed the globals.
For example whenever a plugin adds an annotation, the buffers need
- to be redisplayed. *)
+ to be redisplayed.
+ @since Nitrogen-20111001
+ *)
method protect :
cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> unit) -> unit
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 8cf09cb23d1d209f0371b51cd673904114e636a8..5c225e6121c522ee0115173988ddfea33e608466 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -98,7 +98,7 @@ module Configuration: sig
(** Sets a ConfigInt *)
val find_bool : ?default:bool -> string -> bool
- (** Same as {find_int}. *)
+ (** Same as {!find_int}. *)
val use_bool: string -> (bool -> unit) -> unit
(** Same as {!use_int}. *)
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/scope/defs.mli b/src/plugins/scope/defs.mli
index 862112df114382e986d990583aab1b07dd5a2356..9bc750e6cdf6687b3e74e0027048e705beb6e8f2 100644
--- a/src/plugins/scope/defs.mli
+++ b/src/plugins/scope/defs.mli
@@ -33,5 +33,5 @@ val get_defs_with_type :
val compute_with_def_type_zone:
Cil_types.kernel_function -> Cil_types.stmt -> Locations.Zone.t ->
((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option) option
-(** This function is similar to {get_defs_with_type}, except
+(** This function is similar to {!get_defs_with_type}, except
that it receives a zone as argument, instead of an l-value *)
diff --git a/src/plugins/server/request.mli b/src/plugins/server/request.mli
index 58cfd275a8cd0b598f4d65c8cd37cbe0d1a48549..88fc306b942848e18f0e401a5bbd79f58a68a1ff 100644
--- a/src/plugins/server/request.mli
+++ b/src/plugins/server/request.mli
@@ -170,25 +170,21 @@ val register_sig :
For named input parameters:
[
-
API: Input JSON OCaml Getter
-----------------------------------------------------------------------
Request.param { f: a } 'a (* might raise an exception *)
Request.param ~default { f: a? } 'a (* defined by default *)
Request.param_opt { f: a? } 'a option
-
]
For named output parameters:
[
-
API: Input JSON OCaml Setter
----------------------------------------------------------------------
Request.result { f: a } 'a (* shall be set by process *)
Request.result ~default { f: a } 'a (* defined by default *)
Request.result_opt { f: a? } 'a option
-
]
*)
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/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 346c82aff7689261fb4e1536c91660a51ed19f35..e8536eb1f6e16c262d723f096cf919917e47eb29 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -385,7 +385,7 @@ module type S = sig
(** {3 Transfer Functions } *)
(** Transfer functions from the result of evaluations.
- See {eval.mli} for more details about valuation. *)
+ See {!Eval} for more details about valuation. *)
include Transfer with type state := t
and type value := value
and type location := location
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index b68cb238a08660b37f23a8ba88b178bd601fd56c..3b53316a23cae6666507edafc9fa73385839c680 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -33,7 +33,7 @@ exception Outside_builtin_possibilities
(* Signature of a builtin: type of the result, and type of the arguments. *)
type builtin_type = unit -> typ * typ list
-(** Can the results of a builtin be cached? See {eval.mli} for more details.*)
+(** Can the results of a builtin be cached? See {!Eval} for more details.*)
type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
type full_result = {
diff --git a/src/plugins/value/domains/cvalue/builtins_float.mli b/src/plugins/value/domains/cvalue/builtins_float.mli
index 78eb47efe8504d555207339fc4e54a646006f87c..55070f88b547f56c8172d13b53d1ab3e875e01da 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.mli
+++ b/src/plugins/value/domains/cvalue/builtins_float.mli
@@ -23,7 +23,7 @@
(** Builtins for standard floating-point functions.
Nothing is exported, all the builtins are registered through
- {Builtins.register_builtin} *)
+ {!Builtins.register_builtin} *)
(*
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.mli b/src/plugins/value/domains/cvalue/builtins_memory.mli
index 8a23693e43a9cb320f79aa37dab4b0ed403c71fe..692267d6696d5be14cb722010614c1fd537e8736 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.mli
+++ b/src/plugins/value/domains/cvalue/builtins_memory.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Nothing is exported, all the builtins are registered through
- {Builtins.register_builtin} *)
+ {!Builtins.register_builtin} *)
(*
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index c8f03be0c01f42a72c661500e9e0b3a11e6af28a..141676192e40af40e5e36714274f7c37ec356058 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -25,9 +25,9 @@
(** {2 Registration of abstractions.} *)
(** Dynamic registration of the abstractions to be used in an Eva analysis:
- - value abstractions, detailed in the {Abstract_value} signature;
- - location abstractions, detailed in the {Abstract_location} signature;
- - state abstractions, or abstract domains, detailed in {Abstract_domain}.
+ - value abstractions, detailed in the {!Abstract_value} signature;
+ - location abstractions, detailed in the {!Abstract_location} signature;
+ - state abstractions, or abstract domains, detailed in {!Abstract_domain}.
*)
(** Module types of value abstractions: either a single leaf module, or
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index f894bb7f648fe18d8147e1ac83453af6d48749ce..591dbf95b4735d08beb6707d22e0555cbc2b6047 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -41,7 +41,7 @@ module type S = sig
(** Results of an evaluation: the results of all intermediate calculation (the
value of each expression and the location of each lvalue) are cached here.
- See {eval.mli} for more details. *)
+ See {!Eval} for more details. *)
module Valuation : Valuation with type value = value
and type origin = origin
and type loc = loc
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 1e27948b1c37c0546a37129c71fb4d92d8636232..ed27dd24987432dd38800278ff203a6fa0ea2f7b 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -34,7 +34,7 @@
several times the same leaf module. *)
(** Key and structure for abstract values.
- See {structure.mli} for more details. *)
+ See {!Structure} for more details. *)
module Value : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Value.key
@@ -54,7 +54,7 @@ module Value : sig
end
(** Key and structure for abstract locations.
- See {structure.mli} for more details. *)
+ See {!Structure} for more details. *)
module Location : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Location.key
@@ -74,7 +74,7 @@ module Location : sig
end
(** Key and structure for abstract domains.
- See {structure.mli} for more details. *)
+ See {!Structure} for more details. *)
module Domain : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Domain.key
diff --git a/src/plugins/value/utils/eva_dynamic.mli b/src/plugins/value/utils/eva_dynamic.mli
index 4da1b6c1d7b4e276ffc6e5143c7e9c941acf8827..a51a71a5651e8a6cea0b78a18f017bbea5f0071e 100644
--- a/src/plugins/value/utils/eva_dynamic.mli
+++ b/src/plugins/value/utils/eva_dynamic.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Access to other plugins API via {Dynamic.get}. *)
+(** Access to other plugins API via {!Dynamic.get}. *)
module Callgraph: sig
(** Iterates over all functions in the callgraph in reverse order, i.e. from
diff --git a/src/plugins/value/values/cvalue_backward.mli b/src/plugins/value/values/cvalue_backward.mli
index 37be4507ddeacf37901419d6f6d7aba847184d8e..82d5eef2a3f17f69ab9ca60216bcc095774d72f4 100644
--- a/src/plugins/value/values/cvalue_backward.mli
+++ b/src/plugins/value/values/cvalue_backward.mli
@@ -25,7 +25,7 @@
open Cvalue
open Cil_types
-(** See !{abstract_value.mli} for details about backward operations. *)
+(** See {!Abstract_value} for details about backward operations. *)
(** This function tries to reduce the argument values of a binary operation,
given its result.
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 } *)
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index 559768c449dd3041f13f98809fc657779f1dc6e7..d0dd621be61ad0c176bac679a6f4432424022a1a 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -92,10 +92,10 @@ val c_ptr : unit -> c_int
(** Returns the type of pointers *)
val c_int : ikind -> c_int
-(** Conforms to {Cil.theMachine} *)
+(** Conforms to {!Cil.theMachine} *)
val c_float : fkind -> c_float
-(** Conforms to {Cil.theMachine} *)
+(** Conforms to {!Cil.theMachine} *)
val object_of : typ -> c_object