diff --git a/src/init/boot/boot.ml b/src/init/boot/boot.ml
index 0140f5cb6c53aeb364e47c54cb1ed77ddd316793..db11a81677a0357933082548c3fd3aaf3b688ad0 100644
--- a/src/init/boot/boot.ml
+++ b/src/init/boot/boot.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Frama-C Entry Point (last linked module).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
let play_analysis () =
if Kernel.TypeCheck.get () then begin
diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli
index 09f58c8846332d9b56b989b15a37f8b927baa6b1..21b1100134556d614dd3af4d174aae60852eb592 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -136,7 +136,7 @@ val register_for_loop_body_hook: (Cabs.statement -> unit) -> unit
*)
val register_for_loop_incr_hook: (Cabs.expression -> unit) -> unit
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val convFile: Cabs.file -> Cil_types.file
diff --git a/src/kernel_internals/typing/frontc.mli b/src/kernel_internals/typing/frontc.mli
index 5204f0ae738a7051588e32bc0e90d41bfcc866b5..2bd29fab1e46aaf0637ff57e07ae8626aa01ecba 100644
--- a/src/kernel_internals/typing/frontc.mli
+++ b/src/kernel_internals/typing/frontc.mli
@@ -46,7 +46,7 @@ val setMSVCMode: unit -> unit
(** add a syntactic transformation that will be applied to all freshly parsed
C files.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val add_syntactic_transformation: (Cabs.file -> Cabs.file) -> unit
(** the main command to parse a file. Return a thunk that can be used to
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index e86e3d655329493476ea2aa42181abe0fc72a9f9..0269a087479bec8420c7a9c093882d66b99681c9 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Functors for generic lattices implementations.
- @plugin developer guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
exception Error_Top
(** Raised by some functions when encountering a top value. *)
diff --git a/src/kernel_services/abstract_interp/lattice_type.ml b/src/kernel_services/abstract_interp/lattice_type.ml
index f5e0608d520c6c801358ff9a8c9a478e7cc45036..79c2456447e22286dc3b906c972bdb3b435febdf 100644
--- a/src/kernel_services/abstract_interp/lattice_type.ml
+++ b/src/kernel_services/abstract_interp/lattice_type.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Lattice signatures.
- @plugin developer guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Join_Semi_Lattice = sig
include Datatype.S (** datatype of element of the lattice *)
diff --git a/src/kernel_services/abstract_interp/lmap.mli b/src/kernel_services/abstract_interp/lmap.mli
index 20e1d5f5990d8f942b28d8f8aa23d368c5c4d94b..61069f42fceaeb6c65c47b4274070dad85e1cc5b 100644
--- a/src/kernel_services/abstract_interp/lmap.mli
+++ b/src/kernel_services/abstract_interp/lmap.mli
@@ -22,7 +22,7 @@
(** Maps from bases to memory maps. The memory maps are those of the
[Offsetmap] module.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** Contents of a variable when it is not present in the state.
See function [default_contents] in the functor below *)
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.mli b/src/kernel_services/abstract_interp/lmap_bitwise.mli
index fc44a814aa10fbcfe01d46be8f24b16585949d42..8551bf7244f097ab41c78dcee90d319d96222599 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.mli
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Functors making map indexed by zone.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Locations
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index e071ac4420fcfa507a7e8c648830a58e0d15bc2a..c76b6002c1146de8e6b267ec72d5d70cecea31a9 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -21,12 +21,12 @@
(**************************************************************************)
(** Memory locations.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
(** Association between bases and offsets in byte.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Location_Bytes : sig
(* TODOBY: write an mli for MapLattice, and name the result. Use it there,
and simplify *)
@@ -231,12 +231,12 @@ module Location_Bytes : sig
end
(** Association between bases and offsets in bits.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Location_Bits : module type of Location_Bytes
(** Association between bases and ranges of bits.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Zone : sig
type map_t
@@ -319,13 +319,13 @@ end
(** {2 Locations} *)
(** A {!Location_Bits.t} and a size in bits.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
type location = private {
loc : Location_Bits.t;
size : Int_Base.t;
}
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Location: Datatype.S with type t = location
val loc_bottom : location
@@ -392,7 +392,7 @@ val enumerate_bits : location -> Zone.t
val enumerate_bits_under : location -> Zone.t
val enumerate_valid_bits : access -> location -> Zone.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val enumerate_valid_bits_under : access -> location -> Zone.t
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 485a8c2c3b6724503330b3f0468ae381ee4ad0f5..81e0911b96c4836b5e5a63e538e95cac0aebda85 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -22,7 +22,7 @@
(** Annotations in the AST.
The AST should be computed before calling functions of this module.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
@@ -288,19 +288,19 @@ val add_assert:
Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
(** Add an assertion attached to the given statement. If [kf] is
provided, the function runs faster.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val add_check:
Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
(** Add a checking assertion attached to the given statement. If [kf] is
provided, the function runs faster.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val add_admit:
Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
(** Add an hypothesis assertion attached to the given statement. If [kf] is
provided, the function runs faster.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val add_global: Emitter.t -> global_annotation -> unit
(** Add a new global annotation into the program. *)
diff --git a/src/kernel_services/ast_data/ast.mli b/src/kernel_services/ast_data/ast.mli
index b8fbba2777c77e3f1b1f7196c5bb437d1d8f36b2..4667c234bba5a311e28aaa7f8f6fc54b61785bf5 100644
--- a/src/kernel_services/ast_data/ast.mli
+++ b/src/kernel_services/ast_data/ast.mli
@@ -56,7 +56,7 @@ val get: unit -> Cil_types.file
@raise Bad_Initialization if neither {!File.init_from_c_files}
nor {!File.init_project_from_cil_file} nor {!File.init_from_cmdline} was
called before.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val compute: unit -> unit
(** Enforce the computation of the AST.
@@ -71,14 +71,14 @@ val mark_as_changed: unit -> unit
(** call this function whenever you've made some changes in place
inside the AST
@since Oxygen-20120901
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val mark_as_grown: unit -> unit
(** call this function whenever you have added something to the AST,
without modifying the existing nodes
@since Oxygen-20120901
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val add_monotonic_state: State.t -> unit
@@ -88,12 +88,12 @@ val add_monotonic_state: State.t -> unit
not erase such states, while {!Ast.mark_as_changed} and clearing Ast.self
itself will.
@since Oxygen-20120901
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val self: State.t
(** The state kind associated to the cil AST.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val apply_after_computed: (Cil_types.file -> unit) -> unit
(** Apply the given hook just after building the AST.
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 5e3bd30bf63a7d4ea8fe48c20011d4c9c2616778..9071268fc3b06396fe7c21b5aa185d11d15fac28 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -42,7 +42,7 @@
(****************************************************************************)
(** The Abstract Syntax of CIL.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(**************************** WARNING ***************************************)
(* Remember to reflect any change here into the visitor and pretty-printer *)
@@ -68,7 +68,7 @@
{!Cil.dummyFile} when you need a {!Cil_types.file} as a placeholder. For
each global item CIL stores the source location where it appears (using the
type {!Cil_types.location})
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
type file = {
mutable fileName: Filepath.Normalized.t; (** The complete file name *)
@@ -92,7 +92,7 @@ type file = {
(** The main type for representing global declarations and definitions. A list
of these form a CIL file. The order of globals in the file is generally
important.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and global =
| GType of typeinfo * location
(** A typedef. All uses of type names (through the [TNamed] constructor)
@@ -339,7 +339,7 @@ and attrparam =
(** The definition of a structure or union type. Use {!Cil.mkCompInfo} to make
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
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
and compinfo = {
mutable cstruct: bool;
@@ -387,7 +387,7 @@ and compinfo = {
with the type of the field). *)
(** Information about a struct/union field.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and fieldinfo = {
mutable fcomp: compinfo;
(** The host structure that contains this field. There can be only one
@@ -447,7 +447,7 @@ and fieldinfo = {
enumeration. Make sure you have a [GEnumTag] for each of these. *)
(** Information about an enumeration.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and enuminfo = {
eorig_name: string; (** original name as found in C file. *)
@@ -476,7 +476,7 @@ and enumitem = {
}
(** Information about a defined type.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and typeinfo = {
torig_name: string; (** original name as found in C file. *)
@@ -521,7 +521,7 @@ and typeinfo = {
formals. *)
(** Information about a variable.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and varinfo = {
mutable vname: string;
(** The name of the variable. Cannot be empty. It is primarily your
@@ -684,7 +684,7 @@ and exp_node =
| BinOp of binop * exp * exp * typ
(** Binary operation. Includes the type of the result. The arithmetic
conversions are made explicit for the arguments.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| CastE of typ * exp
(** Use {!Cil.mkCast} to make casts. *)
@@ -756,9 +756,9 @@ and binop =
| MinusPP (** pointer - pointer *)
| Mult (** * *)
| Div (** /
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Mod (** %
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Shiftlt (** shift left *)
| Shiftrt (** shift right *)
@@ -846,7 +846,7 @@ and lhost =
certain kinds of lvalues and its effect is that it advances the starting
address of the lvalue and changes the denoted type, essentially focussing
to some smaller lvalue that is contained in the original one.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and offset =
| NoOffset
(** No offset. Can be applied to any lvalue and does not change either the
@@ -934,7 +934,7 @@ and local_init =
{!Cil.makeFormalVar} and {!Cil.setFormals}. *)
(** Function definitions.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and fundec = {
mutable svar: varinfo;
(** Holds the name and type as a variable, so we can refer to it easily
@@ -1022,7 +1022,7 @@ and block = {
{!Cfg.computeCFGInfo} to do it. *)
(** Statements.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and stmt = {
mutable labels: label list;
(** Whether the statement starts with some labels, case statements or
@@ -1068,11 +1068,11 @@ and stmtkind =
| Instr of instr
(** An instruction that does not contain control flow. Control implicitly
falls through.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Return of exp option * location
(** The return statement. This is a leaf in the CFG.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Goto of stmt ref * location
(** A goto statement. Appears from actual goto's in the code or from goto's
@@ -1080,21 +1080,21 @@ and stmtkind =
statement that is the target of the Goto. This means that you have to
update the reference whenever you replace the target statement. The
target statement MUST have at least a label.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Break of location
(** A break to the end of the nearest enclosing Loop or Switch.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Continue of location
(** A continue to the start of the nearest enclosing [Loop].
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| If of exp * block * block * location
(** A conditional. Two successors, the "then" and the "else" branches (in
this order).
Both branches fall-through to the successor of the If statement.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Switch of exp * block * (stmt list) * location
(** A switch statement. [exp] is the index of the switch. [block] is
@@ -1104,7 +1104,7 @@ and stmtkind =
cannot appear more than once in the list, and statements in
[stmt list] can have several labels corresponding to several
cases.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Loop of
code_annotation list * block * location * (stmt option) * (stmt option)
@@ -1113,12 +1113,12 @@ and stmtkind =
first stmt option will point to the stmt containing the continue label
for this loop and the second will point to the stmt containing the break
label for this loop.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Block of block
(** Just a block of statements. Use it as a way to keep some block attributes
local.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| UnspecifiedSequence of (stmt * lval list
* lval list * lval list * stmt ref list) list
@@ -1148,7 +1148,7 @@ and stmtkind =
In case you do not care about this feature just handle it
like a block (see {!Cil.block_from_unspecified_sequence}).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Throw of (exp * typ) option * location
(** Throws an exception, C++ style.
@@ -1165,7 +1165,7 @@ and stmtkind =
(** On MSVC we support structured exception handling. This is what you might
expect. Control can get into the finally block either from the end of the
body block, or if an exception is thrown.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| TryExcept of block * (instr list * exp) * block * location
(** On MSVC we support structured exception handling. The try/except
@@ -1183,7 +1183,7 @@ and stmtkind =
After that, depending on the value of the expression the control
goes to the handler, propagates the exception, or retries the
exception. The location corresponds to the try keyword.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** Kind of exceptions that are caught by a given clause. *)
and catch_binder =
@@ -1430,7 +1430,7 @@ and term_offset =
(** index. Note that a range is denoted by [TIndex(Trange(i1,i2),ofs)] *)
(** description of a logic function or predicate.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and logic_info = {
(*
mutable l_name : string; (** name of the function. *)
@@ -1464,7 +1464,7 @@ and logic_body =
(** inductive definition *)
(** Description of a logic type.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and logic_type_info = {
mutable lt_name: string;
lt_params : string list; (** type parameters*)
@@ -1490,7 +1490,7 @@ and logic_var_kind =
| LVLocal (** local \let *)
(** description of a logic variable
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and logic_var = {
mutable lv_name : string; (** name of the variable. *)
mutable lv_id : int; (** unique identifier *)
@@ -1505,7 +1505,7 @@ and logic_var = {
}
(** Description of a constructor of a logic sum-type.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and logic_ctor_info =
{ mutable ctor_name: string; (** name of the constructor. *)
ctor_type: logic_type_info; (** type to which the constructor belongs. *)
@@ -1527,7 +1527,7 @@ and relation =
| Rle
| Rge
| Req
- | Rneq (** @plugin development guide *)
+ | Rneq (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** predicates *)
@@ -1657,7 +1657,7 @@ and spec = {
different levels (e.g. [global] and [behavior]), as this would make the
grammar ambiguous.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and acsl_extension = {
ext_id : int;
ext_name : string;
@@ -1666,7 +1666,7 @@ and acsl_extension = {
ext_kind : acsl_extension_kind
}
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and acsl_extension_kind =
| Ext_id of int (** id used internally by the extension itself. *)
| Ext_terms of term list
@@ -1675,7 +1675,7 @@ and acsl_extension_kind =
| Ext_annot of string * acsl_extension list
(** Where are we expected to find corresponding extension keyword.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since 18.0-Argon
*)
and ext_category =
@@ -1702,7 +1702,7 @@ and behavior = {
mutable b_allocation : allocation; (** frees, allocates. *)
mutable b_extended : acsl_extension list
(** extensions
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
}
(** kind of termination a post-condition applies to. See ACSL manual. *)
@@ -1851,7 +1851,7 @@ type syntactic_scope =
belongs. *)
(** Definition of a machine model (architecture + compiler).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
type mach = {
sizeof_short: int; (* Size of "short" *)
sizeof_int: int; (* Size of "int" *)
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index fe2b181766a2d67c8e146a76f1d0d7e2a7b94b6b..2ae3a939ec7f7f64f9eac03812de91dd0022d011 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Operations on globals.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
@@ -99,7 +99,7 @@ module Functions: sig
val get: varinfo -> kernel_function
(** @raise Not_found if the given varinfo has no associated kernel function
and is not a built-in.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val get_params: kernel_function -> varinfo list
val get_vi: kernel_function -> varinfo
@@ -286,7 +286,7 @@ val set_entry_point : string -> bool -> unit
[Kernel.LibEntry] to [lib].
Moreover, clear the results of all the analysis which depend on
[Kernel.MainFunction] or [Kernel.LibEntry].
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_entry_point : ?when_lib_entry:bool -> kernel_function -> bool
(** @return [true] iff the given kernel function is the entry point.
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 0c954057a436afbac342fdb608cfb937cf405271..ce21b069f5d56d7070e2f904bdbbece6b33ebf95 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -25,7 +25,7 @@
functions (like iterators over kernel functions). This kind of operations is
stored in module {!Globals.Functions}.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
@@ -209,7 +209,7 @@ val is_return_stmt: t -> stmt -> bool
(* ************************************************************************* *)
val dummy: unit -> t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val get_vi : t -> varinfo
val get_id: t -> int
@@ -230,7 +230,7 @@ val get_statics : t -> varinfo list
exception No_Definition
val get_definition : t -> fundec
(** @raise No_Definition if the given function is not a definition.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val has_definition : t -> bool
(** @return [true] iff the given kernel function has a defintion.
@@ -269,7 +269,7 @@ val get_called : exp -> t option
(* ************************************************************************* *)
(** Hashtable indexed by kernel functions and dealing with project.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Make_Table(Data: Datatype.S)(Info: State_builder.Info_with_size):
State_builder.Hashtbl with type key = t and type data = Data.t
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index eaf6c8bc0db251ebc066d74efacee36d742d1a6b..af54a56f5721c77d18783a3897b1154558f7e86c 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -22,7 +22,7 @@
(** ACSL comparable property.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 3252bc6eaf56fda2255248801eb65f64cddcf8ca..bbe2f162668e8d475022dc3730dd77d5d541cd79 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -22,7 +22,7 @@
(** Status of properties.
@since Nitrogen-20111001
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************ *)
(** {2 Local status}
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index a651c98bf1f72df4f4ded14dda5d38bdcfaca299..6b581a5ec04b8b33ce937789375801bdd1676f4e 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -95,7 +95,7 @@ type extension_printer =
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = Acsl_extension.register_behavior "FOO" foo_typer false
]
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_behavior:
string -> ?preprocessor:extension_preprocessor -> extension_typer ->
@@ -105,7 +105,7 @@ val register_behavior:
(** Registers extension for global annotation. See [register_behavior].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_global:
string -> ?preprocessor:extension_preprocessor -> extension_typer ->
@@ -115,7 +115,7 @@ val register_global:
(** Registers extension for global block annotation. See [register_behavior].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_global_block:
string -> ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
@@ -126,7 +126,7 @@ val register_global_block:
(** Registers extension for code annotation to be evaluated at _current_
program point. See [register_behavior].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_code_annot:
string -> ?preprocessor:extension_preprocessor -> extension_typer ->
@@ -137,7 +137,7 @@ val register_code_annot:
(** Registers extension for code annotation to be evaluated for the _next_
statement. See [register_behavior].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_code_annot_next_stmt:
string -> ?preprocessor:extension_preprocessor -> extension_typer ->
@@ -147,7 +147,7 @@ val register_code_annot_next_stmt:
(** Registers extension for loop annotation. See [register_behavior].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_code_annot_next_loop:
string -> ?preprocessor:extension_preprocessor -> extension_typer ->
@@ -158,7 +158,7 @@ val register_code_annot_next_loop:
(** Registers extension both for code and loop annotations.
See [register_behavior].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val register_code_annot_next_both:
string -> ?preprocessor:extension_preprocessor -> extension_typer ->
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index ac92bae3b7cd470496dde5687a6123f1611eda21..d673ff60b03f5b82e94adb9a45866a968bff9d21 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -46,7 +46,7 @@
CIL original API documentation is available as
an html version at http://manju.cs.berkeley.edu/cil.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
open Cil_datatype
@@ -1079,7 +1079,7 @@ val mkEmptyStmt: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
val dummyInstr: instr
(** A statement consisting of just [dummyInstr].
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val dummyStmt: stmt
(** Create an instruction equivalent to a pure expression. The new instruction
@@ -1488,33 +1488,33 @@ val isWFGhostType : typ -> bool
(** Different visiting actions. 'a will be instantiated with [exp], [instr],
etc.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
type 'a visitAction =
| SkipChildren (** Do not visit the children. Return the node as it is.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| DoChildren (** Continue with the children of this node. Rebuild the node on
return if any of the children changes (use == test).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| DoChildrenPost of ('a -> 'a)
(** visit the children, and apply the given function to the result.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| JustCopy (** visit the children, but only to make the necessary copies
(only useful for copy visitor).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| JustCopyPost of ('a -> 'a)
(** same as JustCopy + applies the given function to the result.
- @plugin development guide*)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide*)
| ChangeTo of 'a (** Replace the expression with the given one.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| ChangeToPost of 'a * ('a -> 'a)
(** applies the expression to the function and gives back the result.
Useful to insert some actions in an inheritance chain.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| ChangeDoChildrenPost of 'a * ('a -> 'a)
(** First consider that the entire exp is replaced by the first parameter. Then
continue with the children. On return rebuild the node if any of the
children has changed and then apply the function on the node.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val mk_behavior :
?name:string ->
@@ -1561,11 +1561,11 @@ val find_default_requires: behavior list -> identified_predicate list
{!Visitor.generic_frama_c_visitor} instead of {!genericCilVisitor} or
{!nopCilVisitor}
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
class type cilVisitor = object
method behavior: Visitor_behavior.t
(** the kind of behavior expected for the behavior.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method project: Project.t option
(** Project the visitor operates on. Non-nil for copy visitor.
@@ -1576,7 +1576,7 @@ class type cilVisitor = object
method vfile: file -> file visitAction
(** visit a whole file.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vvdec: varinfo -> varinfo visitAction
(** Invoked for each variable declaration. The children to be traversed
@@ -1586,20 +1586,20 @@ class type cilVisitor = object
formals and locals of function definitions. This means that the list
of formals of a function may be traversed multiple times if there exists
both a declaration and a definition, or multiple declarations.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vvrbl: varinfo -> varinfo visitAction
(** Invoked on each variable use. Here only the [SkipChildren] and
[ChangeTo] actions make sense since there are no subtrees. Note that
the type and attributes of the variable are not traversed for a
variable use.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vexpr: exp -> exp visitAction
(** Invoked on each expression occurrence. The subtrees are the
subexpressions, the types (for a [Cast] or [SizeOf] expression) or the
variable use.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlval: lval -> lval visitAction
(** Invoked on each lvalue occurrence *)
@@ -1608,7 +1608,7 @@ class type cilVisitor = object
(** Invoked on each offset occurrence that is *not* as part of an
initializer list specification, i.e. in an lval or recursively inside an
offset.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vinitoffs: offset -> offset visitAction
(** Invoked on each offset appearing in the list of a
@@ -1625,7 +1625,7 @@ class type cilVisitor = object
[Goto] and [Case] statements that point to the original statement. If you
use the [ChangeTo] action then you should take care of preserving that
sharing yourself.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vblock: block -> block visitAction
(** Block. *)
@@ -1635,7 +1635,7 @@ class type cilVisitor = object
method vglob: global -> global list visitAction
(** Global (vars, types, etc.)
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vinit: varinfo -> offset -> init -> init visitAction
(** Initializers. Pass the global where this occurs, and the offset *)
@@ -1687,7 +1687,7 @@ class type cilVisitor = object
(** [Kstmt stmt] when visiting statement stmt, [Kglobal] when called outside
of a statement.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method push_stmt : stmt -> unit
method pop_stmt : stmt -> unit
@@ -1710,29 +1710,29 @@ class type cilVisitor = object
method vterm_offset: term_offset -> term_offset visitAction
method vlogic_label: logic_label -> logic_label visitAction
method vlogic_info_decl: logic_info -> logic_info visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_info_use: logic_info -> logic_info visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_type_info_decl: logic_type_info -> logic_type_info visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_type_info_use: logic_type_info -> logic_type_info visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_type_def: logic_type_def -> logic_type_def visitAction
method vlogic_ctor_info_decl: logic_ctor_info -> logic_ctor_info visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_ctor_info_use: logic_ctor_info -> logic_ctor_info visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_var_decl: logic_var -> logic_var visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vlogic_var_use: logic_var -> logic_var visitAction
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method vquantifiers: quantifiers -> quantifiers visitAction
@@ -1768,11 +1768,11 @@ class type cilVisitor = object
method fill_global_tables: unit
(** fill the global environment tables at the end of a full copy in a
new project.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method get_filling_actions: (unit -> unit) Queue.t
(** get the queue of actions to be performed at the end of a full copy.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
end
@@ -1826,19 +1826,19 @@ val doVisitList:
(** Visit a file. This will re-cons all globals TWICE (so that it is
* tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will
* not change the list of globals.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val visitCilFileCopy: cilVisitor -> file -> file
(** Same thing, but the result is ignored. The given visitor must thus be
an inplace visitor. Nothing is done if the visitor is a copy visitor.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val visitCilFile: cilVisitor -> file -> unit
(** A visitor for the whole file that does not *physically* change the
globals (but maybe changes things inside the globals through
side-effects). Use this function instead of {!Cil.visitCilFile}
whenever appropriate because it is more efficient for long files.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val visitCilFileSameGlobals: cilVisitor -> file -> unit
(** Same as {!visitCilFilesSameGlobals}, but only visits function definitions
@@ -2272,7 +2272,7 @@ val cvar_to_term: loc:location -> varinfo -> term
val make_temp_logic_var: logic_type -> logic_var
(** The constant logic term zero.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val lzero : ?loc:location -> unit -> term
(** The constant logic term 1. *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 807648fbb378e86a9e0df39f6810bc800242db47..db708394580d03cf24cfb968f10feed718f3af96 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Datatypes of some useful CIL types.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* This module should not be exported, but we need the alias and OCaml
requires us to export it. *)
@@ -259,7 +259,7 @@ module Typeinfo: S_with_collections with type t = typeinfo
module Varinfo_Id: Hptmap.Id_Datatype with type t = varinfo
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Varinfo: sig
include S_with_collections_pretty with type t = varinfo
module Hptset: sig
diff --git a/src/kernel_services/ast_queries/cil_state_builder.mli b/src/kernel_services/ast_queries/cil_state_builder.mli
index 516ac23c060daeeb7bc6e86fadc1568e2b52514d..cd5240d4ac97fd1f3405ea387d7786c278278445 100644
--- a/src/kernel_services/ast_queries/cil_state_builder.mli
+++ b/src/kernel_services/ast_queries/cil_state_builder.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Functors for building computations which use kernel datatypes.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Stmt_set_ref(Info: State_builder.Info) :
State_builder.Set_ref with type elt = Cil_types.stmt
@@ -29,7 +29,7 @@ module Stmt_set_ref(Info: State_builder.Info) :
module Kinstr_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.kinstr and type data = Data.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Stmt_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.stmt and type data = Data.t
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 8042cf4420e9f471b83b2c6d9dc6ae000bd45e90..10473c5178bb005926953ea4ea2b1e84b601aceb 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -50,7 +50,7 @@ val new_file_type:
string -> (string -> Cil_types.file * Cabs.file) -> unit
(** [new_file_type suffix func funcname] registers a new type of files (with
corresponding suffix) as recognized by Frama-C through [func].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val new_machdep: string -> Cil_types.mach -> unit
@@ -60,7 +60,7 @@ val new_machdep: string -> Cil_types.mach -> unit
(fun () -> File.new_machdep "my_machdep" my_machdep_implem)]
@since Nitrogen-20111001
@raise Invalid_argument if the given name already exists
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val machdep_macro: string -> string
(** [machdep_macro machine] returns the name of a macro __FC_MACHDEP_XXX so
@@ -110,7 +110,7 @@ val add_code_transformation_before_cleanup:
At this level, globals and ACSL annotations have not been registered.
@since Neon-20140301
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val add_code_transformation_after_cleanup:
?deps:(module Parameter_sig.S) list ->
@@ -124,7 +124,7 @@ val add_code_transformation_after_cleanup:
Note that it is the responsibility of the hook to use
{!Ast.mark_as_changed} or {!Ast.mark_as_grown} whenever it is the case.
@since Neon-20140301
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val constfold: code_transformation_category
(** category for syntactic constfolding (done after cleanup)
@@ -135,7 +135,7 @@ val must_recompute_cfg: Cil_types.fundec -> unit
when they modify statements in function [f]. This will trigger a
recomputation of the cfg of [f] after the transformation.
@since Neon-20140301
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val get_suffixes: unit -> string list
(** @return the list of accepted suffixes of input source files
@@ -172,14 +172,14 @@ val init_from_c_files: t list -> unit
(** Initialize the cil file representation of the current project.
Should be called at most once per project.
@raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val init_project_from_cil_file: Project.t -> Cil_types.file -> unit
(** Initialize the cil file representation with the given file for the
given project from the current one.
Should be called at most once per project.
@raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val init_project_from_visitor:
?reorder:bool -> Project.t -> Visitor.frama_c_visitor -> unit
@@ -190,7 +190,7 @@ val init_project_from_visitor:
if [reorder] is [true] (default is [false]) the new AST in [prj]
will be reordered.
@since Oxygen-20120901
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val create_project_from_visitor:
@@ -207,7 +207,7 @@ val create_project_from_visitor:
file (i.e. it should use {!Cil.copy_visit} at some point).
@raise File_types.Bad_Initialization if called more than once.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val create_rebuilt_project_from_visitor:
?reorder:bool -> ?last:bool -> ?preprocess:bool ->
@@ -233,7 +233,7 @@ val init_from_cmdline: unit -> unit
command line.
Should be called at most once per project.
@raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val reorder_ast: unit -> unit
(** reorder globals so that all uses of an identifier are preceded by its
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 8b0030707084d570c0765af217a5a9fe898789a8..459a8569510d28889fdc4f2ca6e1e1108fa6efde 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -25,7 +25,7 @@
open Cil_types
(** Smart constructors for the logic.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** {1 Identification Numbers} *)
@@ -261,7 +261,7 @@ let addTermOffsetLval toadd (b, off) : term_lval =
(** {2 Terms} *)
(* empty line for ocamldoc *)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
let term ?(loc=Cil_datatype.Location.unknown) term typ =
{ term_node = term;
term_type = typ;
@@ -406,7 +406,7 @@ let piff ?(loc=Cil_datatype.Location.unknown) (p2,p3) =
| _, Ptrue -> p2
| _,_ -> unamed ~loc (Piff (p2,p3))
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
let prel ?(loc=Cil_datatype.Location.unknown) (a,b,c) =
unamed ~loc (Prel(a,b,c))
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 2a7d97c98f428e97ff7f5cbba534aa74270a7f91..5bbc7457d3e8f2e574fd4845811ffc42b4e8da7c 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -23,7 +23,7 @@
(**************************************************************************)
(** Smart constructors for logic annotations.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
open Cil_datatype
@@ -65,7 +65,7 @@ val toplevel_predicate: ?kind:predicate_kind -> predicate -> toplevel_predicate
val new_predicate: ?kind:predicate_kind -> predicate -> identified_predicate
(** creates a new acsl_extension with a fresh id.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Chlorine-20180501
*)
val new_acsl_extension:
@@ -162,7 +162,7 @@ val pif:
val piff: ?loc:location -> predicate * predicate -> predicate
(** Binary relation.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val prel: ?loc:location -> relation * term * term -> predicate
(** \forall *)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 4eebe17c00c05b56947bb482285c5da60d2a8c35..7784937d3abd6a1e46e547ae9cece351118c0cc4 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -125,7 +125,7 @@ type typing_context = {
possible for the extension to change the type-checking functions for
the sub-nodes of the parsed tree, and not only for the toplevel [lexpr].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
type_term:
typing_context -> Lenv.t -> Logic_ptree.lexpr -> term;
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 307d889ee9baf44ceba4c59e987148605fc3c068..a7ea2707d7e7a1388606de36401686f7c068a2f3 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -23,7 +23,7 @@
(**************************************************************************)
(** Utilities for ACSL constructs.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
@@ -33,7 +33,7 @@ exception Not_well_formed of location * string
(** basic utilities for logic terms and predicates. See also {! Logic_const}
to build terms and predicates.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** add a logic function in the environment.
See {!Logic_env.add_logic_function_gen}*)
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index d335b4e10dd0dd079888298df2c681a58a77c64e..420e6b58ef55031157646d40a2be2e01f5c3f1f4 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Command line parsing.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************** *)
(** {2 Stage configurations}
@@ -33,39 +33,39 @@
type stage =
| Early (** Initial stage for very specific almost hard-coded
options. Do not use it.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Extending (** Before loading plug-ins. Run only once.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Extended (** The stage where plug-ins are loaded.
It is also the first stage each time the Frama-C main
loop is run (e.g. after each "-then").
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Exiting (** Run once when exiting Frama-C.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Loading (** After {!Extended}, the stage where a previous Frama-C
internal states is restored (e.g. the one specified by
-load or by running the journal).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Configuring (** The stage where all the parameters which were not already
set may be modified to take into account cmdline options.
Just after this stage, Frama-C will run the plug-in mains.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** The different stages, from the first to be executed to the last one.
@since Beryllium-20090601-beta1 *)
val run_after_early_stage: (unit -> unit) -> unit
(** Register an action to be executed at the end of the early stage.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090901 *)
val run_during_extending_stage: (unit -> unit) -> unit
(** Register an action to be executed during the extending stage.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090901 *)
val run_after_extended_stage: (unit -> unit) -> unit
(** Register an action to be executed at the end of the extended stage.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090901 *)
type exit
@@ -73,21 +73,21 @@ type exit
val nop : exit
(** @since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
exception Exit
(** @since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val run_after_exiting_stage: (unit -> exit) -> unit
(** Register an action to be executed at the end of the exiting stage.
The guarded action must finish by [exit n].
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090601-beta1 *)
val run_after_loading_stage: (unit -> unit) -> unit
(** Register an action to be executed at the end of the loading stage.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090601-beta1 *)
val is_going_to_load: unit -> unit
@@ -95,17 +95,17 @@ val is_going_to_load: unit -> unit
It is not necessary to call this function if the running action is set by
an option put on the command line.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val run_after_configuring_stage: (unit -> unit) -> unit
(** Register an action to be executed at the end of the configuring stage.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090601-beta1 *)
val run_after_setting_files: (string list -> unit) -> unit
(** Register an action to be executed just after setting the files put on the
command line. The argument of the function is the list of files.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Carbon-20101201 *)
val at_normal_exit: (unit -> unit) -> unit
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index 2d2d03cc876ed18a95b05afd0f0e1a012a1163dd..f29dad1f049c04a2aae163be15ca5c630482a6ee 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli
@@ -26,7 +26,7 @@
provided by the functor {!Plugin.Register} and generating a new
parameter.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val set_cmdline_stage: Cmdline.stage -> unit
(** Set the stage where the option corresponding to the parameter is
@@ -58,7 +58,7 @@ val set_negative_option_name: string -> unit
Assume that the given string is a valid option name or empty.
If it is empty, no negative option is created.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val set_negative_option_help: string -> unit
(** For boolean parameters, set the help message of the negative
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml
index b5558a5aa42f0b5a808ff2402cb2480d6afc9354..e032660b655222f1a79e1d730d0e6aff30886573 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml
@@ -216,7 +216,7 @@ end
(* ************************************************************************** *)
(** Signature for a boolean parameter.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Bool = sig
include S with type t = bool
@@ -230,7 +230,7 @@ module type Bool = sig
end
(** Signature for an integer parameter.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Int = sig
include S with type t = int
@@ -437,7 +437,7 @@ module type String_set =
(** Set of defined kernel functions. If you want to also include pure
prototype, use {!Parameter_customize.argument_may_be_fundecl}.
@since Sodium-20150201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Kernel_function_set =
Set with type elt = Cil_types.kernel_function
and type t = Cil_datatype.Kf.Set.t
@@ -515,7 +515,7 @@ module type Filepath_map =
(** Signatures containing the different functors which may be used to generate
new command line options.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Builder = sig
val no_element_of_string: string -> 'a
@@ -526,26 +526,26 @@ module type Builder = sig
module Bool(X:sig include Input val default: bool end): Bool
module Action(X: Input) : Bool
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module False(X: Input) : Bool
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module True(X: Input) : Bool
module WithOutput
(X: sig include Input val output_by_default: bool end):
With_output
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Int(X: sig include Input_with_arg val default: int end): Int
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Zero(X: Input_with_arg): Int
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module String(X: sig include Input_with_arg val default: string end): String
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Empty_string(X: Input_with_arg): String
module Fc_Filepath = Filepath
@@ -568,7 +568,7 @@ module type Builder = sig
(X: sig include Input_collection val default: E.Set.t end):
Set with type elt = E.t and type t = E.Set.t
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module String_set(X: Input_with_arg): String_set
module Filled_string_set
@@ -577,7 +577,7 @@ module type Builder = sig
val default: Datatype.String.Set.t
end): String_set
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Kernel_function_set(X: Input_with_arg): Kernel_function_set
module Fundec_set(X: Input_with_arg): Fundec_set
diff --git a/src/kernel_services/cmdline_parameters/parameter_state.mli b/src/kernel_services/cmdline_parameters/parameter_state.mli
index aabe1efd6e247cf30a70a9d670d57dd2477bb5fa..8051e561be0c271ac7ee157306ed166f988bb734 100644
--- a/src/kernel_services/cmdline_parameters/parameter_state.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_state.mli
@@ -33,7 +33,7 @@ val get_selection: ?is_set:bool -> unit -> State_selection.t
[is_set] is [true] by default (for backward compatibility): in such a
case, for each option, the extra internal state indicating whether it is
set also belongs to the selection.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val get_reset_selection: ?is_set:bool -> unit -> State_selection.t
(** Selection of resettable parameters in case of copy with a visitor.
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index 5313481fd20a90ef97ce08562d05128293185d6c..309a515159c8e40cb3c7c78826ce85f3c482c475 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -42,7 +42,7 @@
(****************************************************************************)
(** Untyped AST.
- @plugin development guide **)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide **)
(*
** Types
@@ -175,7 +175,7 @@ and definition =
| GLOBANNOT of Logic_ptree.decl list
(** the file name, and then the list of toplevel forms.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
and file = Datatype.Filepath.t * (bool * definition) list
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 0c37f844ea026f80172eb505e9d567e5c5d63b7d..e254132ee264d2cb89d160640ee467d6248ff938 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Database in which static plugins are registered.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(**
Modules providing general services:
@@ -83,12 +83,12 @@ val register_guarded_compute:
(** Frama-C main interface.
@since Lithium-20081201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Main: sig
val extend : (unit -> unit) -> unit
(** Register a function to be called by the Frama-C main entry point.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val play: (unit -> unit) ref
(** Run all the Frama-C analyses. This function should be called only by
@@ -132,7 +132,7 @@ module Value : sig
val self : State.t
(** Internal state of the value analysis from projects viewpoint.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val mark_as_computed: unit -> unit
(** Indicate that the value analysis has been done already. *)
@@ -144,11 +144,11 @@ module Value : sig
@raise Db.Value.Incorrect_number_of_arguments if some arguments are
specified for the entry point using {!Db.Value.fun_set_args}, and
an incorrect number of them is given.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_computed: unit -> bool
(** Return [true] iff the value analysis has been done.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Table_By_Callstack:
State_builder.Hashtbl with type key = stmt
@@ -243,7 +243,7 @@ module Value : sig
val get_stmt_state : ?after:bool -> stmt -> state
(** [after] is false by default.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val fold_stmt_state_callstack :
(state -> 'a -> 'a) -> 'a -> after:bool -> stmt -> 'a
@@ -308,7 +308,7 @@ module Value : sig
val is_accessible : kinstr -> bool
val is_reachable : state -> bool
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_reachable_stmt : stmt -> bool
@@ -580,7 +580,7 @@ end
(* ************************************************************************* *)
(** Dealing with logical properties.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Properties : sig
(** Interpretation of logic terms. *)
@@ -1274,7 +1274,7 @@ module Derefs : INOUT with type t = Locations.Zone.t
(** This function should be called from time to time by all analysers taking
time. In GUI mode, this will make the interface reactive.
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@deprecated 21.0-Scandium *)
val progress: (unit -> unit) ref
[@@ deprecated "Use Db.yield instead."]
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index 070fc65597090ddf05bffadd049c85a2e52b46a4..2dcdd083b7adb2d6eab12cf876bbb47857aec3fd 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Value accesses through dynamic typing.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************* *)
(** {2 Registration} *)
@@ -35,7 +35,7 @@ val register:
[name], the type [ty] and the plug-in [plugin].
@raise Type.AlreadyExists if [name] already exists. In other words you
cannot register a value with the same name twice.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************* *)
(** {2 Access} *)
@@ -58,7 +58,7 @@ val get: plugin:string -> string -> 'a Type.t -> 'a
@raise Incompatible_type if the name is not registered
with a compatible type
@raise Failure _ in the -no-obj mode
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val iter: (string -> 'a Type.t -> 'a -> unit) -> unit
val iter_comment : (string -> string -> unit) -> unit
@@ -70,7 +70,7 @@ val iter_comment : (string -> string -> unit) -> unit
(** Module to use for accessing parameters of plug-ins.
Assume that the plug-in is already loaded.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Parameter : sig
(** Set of common operations on parameters. *)
@@ -98,7 +98,7 @@ module Parameter : sig
(**/**)
(** Boolean parameters.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Bool: sig
include Common with type t = bool
val on: string -> unit -> unit
diff --git a/src/kernel_services/plugin_entry_points/emitter.mli b/src/kernel_services/plugin_entry_points/emitter.mli
index 0da83cb0b710ac6047360386ad0213799464dfbf..96e4ae157d547da175a300d28f0a2def5ef33e85 100644
--- a/src/kernel_services/plugin_entry_points/emitter.mli
+++ b/src/kernel_services/plugin_entry_points/emitter.mli
@@ -49,7 +49,7 @@ val create:
become valid or invalid, but a valid status cannot become invalid).
The given name must be unique.
@raise Invalid_argument if an emitter with the given name already exist
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val get_name: t -> string
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
index f9be3ee7a31b714322c560bbe4e62871328f29e5..33fb39a20b84e121720de6d569cd976e21739971 100644
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ b/src/kernel_services/plugin_entry_points/journal.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Journalization of functions.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ****************************************************************************)
(** {2 Journalization} *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index b58ecaa79ad262e327b13fb21811893d43e33080..ee8a7b424fcd4f5ed9e2592738a0d95730d8705f 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Provided services for kernel developers.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************* *)
(** {2 Log Machinery} *)
@@ -285,14 +285,14 @@ module Quiet: Parameter_sig.Bool
module Permissive: Parameter_sig.Bool
(** Behavior of option "-permissive" *)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Unicode: sig
include Parameter_sig.Bool
val without_unicode: ('a -> 'b) -> 'a -> 'b
(** Execute the given function as if the option [-unicode] was not set. *)
end
(** Behavior of option "-unicode".
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Time: Parameter_sig.String
(** Behavior of option "-time" *)
@@ -324,7 +324,7 @@ module PrintReturn : Parameter_sig.Bool
@since Sulfur-20171101 *)
(** Behavior of option "-ocode".
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module CodeOutput : sig
include Parameter_sig.Filepath
val output: (Format.formatter -> unit) -> unit
@@ -584,7 +584,7 @@ module UnspecifiedAccess: Parameter_sig.Bool
module SafeArrays: Parameter_sig.Bool
(** Behavior of option "-safe-arrays".
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module SignedOverflow: Parameter_sig.Bool
(** Behavior of option "-warn-signed-overflow" *)
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index a44b6b4ae22032c9aedd987c3bf90d05d71c1e68..9a83010ddc7cd4b857532497405df29e8c355c20 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -68,7 +68,7 @@ type ('a,'b) pretty_aborter =
(* -------------------------------------------------------------------------- *)
(** {2 Exception Registry}
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
@since Beryllium-20090601-beta1 *)
(* -------------------------------------------------------------------------- *)
@@ -118,7 +118,7 @@ type warn_status =
| Wabort (** emit a message and abort execution *)
(** @since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Messages = sig
type category
@@ -155,45 +155,45 @@ module type Messages = sig
val result : ?level:int -> ?dkey:category -> 'a pretty_printer
(** Results of analysis. Default level is 1.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val feedback : ?ontty:ontty -> ?level:int -> ?dkey:category -> 'a pretty_printer
(** Progress and feedback. Level is tested against the verbosity level.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val debug : ?level:int -> ?dkey:category -> 'a pretty_printer
(** Debugging information dedicated to Plugin developers.
Default level is 1. The debugging key is used in message headers.
See also [set_debug_keys] and [set_debug_keyset].
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val warning : ?wkey:warn_category -> 'a pretty_printer
(** Hypothesis and restrictions.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val error : 'a pretty_printer
(** user error: syntax/typing error, bad expected input, etc.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val abort : ('a,'b) pretty_aborter
(** user error stopping the plugin.
@raise AbortError with the channel name.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val failure : 'a pretty_printer
(** internal error of the plug-in.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val fatal : ('a,'b) pretty_aborter
(** internal error of the plug-in.
@raise AbortFatal with the channel name.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val verify : bool -> ('a,bool) pretty_aborter
(** If the first argument is [true], return [true] and do nothing else,
@@ -202,7 +202,7 @@ module type Messages = sig
The intended usage is: [assert (verify e "Bla...") ;].
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val not_yet_implemented : ?current:bool -> ?source:Filepath.position ->
('a,formatter,unit,'b) format4 -> 'a
@@ -250,7 +250,7 @@ module type Messages = sig
- [log ~verbose:n ~debug:m]: any debugging or verbosity level is
sufficient.
@since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val logwith : (event option -> 'b) ->
?wkey:warn_category -> ?emitwith:(event -> unit) -> ?once:bool ->
@@ -388,7 +388,7 @@ val set_echo : ?plugin:string -> ?kind:kind list -> bool -> unit
(** Turns echo on or off. Applies to all channel unless specified,
and all kind of messages unless specified.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val add_listener : ?plugin:string -> ?kind:kind list -> (event -> unit) -> unit
(** Register a hook that is called each time an event is
@@ -399,7 +399,7 @@ val add_listener : ?plugin:string -> ?kind:kind list -> (event -> unit) -> unit
temporarily deactivated in order to avoid infinite recursion.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val echo : event -> unit
(** Display an event of the terminal, unless echo has been turned off.
@@ -421,13 +421,13 @@ type channel
val new_channel : string -> channel
(** @since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val log_channel : channel ->
?kind:kind -> 'a pretty_printer
(** logging function to user-created channel.
@since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val kernel_channel_name: string
(** the reserved channel name used by the Frama-C kernel.
@@ -454,7 +454,7 @@ val clean : unit -> unit
val set_output : ?isatty:bool -> (string -> int -> int -> unit) -> (unit -> unit) -> unit
(** This function has the same parameters as Format.make_formatter.
@since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val print_on_output : (Format.formatter -> unit) -> unit
(** Direct printing on output.
@@ -464,7 +464,7 @@ val print_on_output : (Format.formatter -> unit) -> unit
Can not be recursively invoked.
@since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val print_delayed : (Format.formatter -> unit) -> unit
(** Direct printing on output. Same as [print_on_output], except
@@ -474,7 +474,7 @@ val print_delayed : (Format.formatter -> unit) -> unit
Can not be recursively invoked.
@since Beryllium-20090901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(**/**)
val set_current_source : (unit -> Filepath.position) -> unit
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 0851fea085914da838db93143510ee60324ed74b..227209f8525e2a85c05f665d5bb2c91e81f21736 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -25,7 +25,7 @@
an ad'hoc manner. Should not be of any use for a standard plug-in,
who would rather rely on {!Plugin.S} below.
@since Chlorine-20180501
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
module type S_no_log = sig
@@ -74,7 +74,7 @@ end
(** Provided plug-general services for plug-ins.
@since Beryllium-20090601-beta1
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type S = sig
include Log.Messages
include S_no_log
@@ -105,7 +105,7 @@ val register_kernel: unit -> unit
(** Functors for registering a new plug-in. It provides access to several
services.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Register
(P: sig
val name: string
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index cbfdfbc2c3f0d07e732ec888097fcac4845d81ec..2319f0376797b78387fcc6ffb2d08d5941485d81 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -35,7 +35,7 @@ class type frama_c_visitor = object
method vstmt_aux: Cil_types.stmt -> Cil_types.stmt visitAction
method vglob_aux: Cil_types.global -> Cil_types.global list visitAction
method current_kf: kernel_function option
- (** @plugin development guide *)
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method set_current_kf: kernel_function -> unit
method reset_current_kf: unit -> unit
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 8469257aaf4bd60e3e2d32ffa9a83a1bbeffa4e5..1413219ed8406bd58488698d92eba9553ac2c2c0 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -59,17 +59,17 @@ class type frama_c_visitor = object
method vstmt_aux: stmt -> stmt Cil.visitAction
(** Replacement of vstmt.
- @plugin development guide*)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide*)
method vglob_aux: global -> global list Cil.visitAction
(** Replacement of vglob.
- @plugin development guide*)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide*)
method current_kf: kernel_function option
(** link to the kernel function currently being visited.
{b NB:} for copy visitors, the link is to the original kf (anyway,
the new kf is created only after the visit is over).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method set_current_kf: kernel_function -> unit
(** Internal use only. *)
@@ -80,7 +80,7 @@ end
class frama_c_inplace: frama_c_visitor
(** in-place visitor; always act in the current project.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
class frama_c_copy: Project.t -> frama_c_visitor
(** Copying visitor. The [Project.t] argument specifies in which project the
@@ -97,7 +97,7 @@ class frama_c_refresh: Project.t -> frama_c_visitor
class generic_frama_c_visitor:
Visitor_behavior.t -> frama_c_visitor
(** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy].
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** Visit a file. This will re-cons all globals TWICE (so that it is
tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will
@@ -112,7 +112,7 @@ val visitFramacFile: frama_c_visitor -> file -> unit
changes things inside the globals). Use this function instead of
{!Visitor.visitFramacFile} whenever appropriate because it is more
efficient for long files.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val visitFramacFileSameGlobals: frama_c_visitor -> file -> unit
(** Visit all function definitions of a file. Use this function instead of
@@ -142,7 +142,7 @@ val visitFramacGlobal: frama_c_visitor -> global -> global list
val visitFramacKf: frama_c_visitor -> Kernel_function.t -> Kernel_function.t
(** Visit a function definition.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val visitFramacFunction: frama_c_visitor -> fundec -> fundec
(** Visit an expression *)
diff --git a/src/kernel_services/visitors/visitor_behavior.mli b/src/kernel_services/visitors/visitor_behavior.mli
index 9e4adf0201f6d0745700fd4f6e2890144bea0bbe..c395d1d848ba077b59090c629e139a6bb75b2791 100644
--- a/src/kernel_services/visitors/visitor_behavior.mli
+++ b/src/kernel_services/visitors/visitor_behavior.mli
@@ -32,11 +32,11 @@ type t
(** How the visitor should behave in front of mutable fields: in
place modification or copy of the structure. This type is abstract.
Use one of the two values below in your classes.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val inplace: unit -> t
(** In-place modification. Behavior of the original cil visitor.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val copy: Project.t -> t
(** Makes fresh copies of the mutable structures.
@@ -46,7 +46,7 @@ val copy: Project.t -> t
AST. This allows for instance to copy a function with its
formals and local variables, and to keep the references to other
globals in the function's body.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val refresh: Project.t -> t
(** Makes fresh copies of the mutable structures and provides fresh id
@@ -74,7 +74,7 @@ val get_project: t -> Project.t option
AST elements in [vis]. For example for {!Cil_types.varinfo}: [Reset.varinfo vis].
@since 20.0-Calcium
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
module Reset: sig
val varinfo: t -> unit
@@ -116,7 +116,7 @@ end
[Get.varinfo vis vi].
@since 20.0-Calcium
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
module Get: Get
@@ -128,7 +128,7 @@ module Get: Get
{!Cil_types.varinfo}: [Get_orig.varinfo vis new_vi].
@since 20.0-Calcium
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
module Get_orig: Get
@@ -141,7 +141,7 @@ module Get_orig: Get
{!Cil_types.varinfo}: [Memo.varinfo vis vi].
@since 20.0-Calcium
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
module Memo: Get
@@ -174,7 +174,7 @@ end
{!Cil_types.varinfo}: [Set.varinfo vis vi new_representative].
@since 20.0-Calcium
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
module Set: Set
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index fb520585b8f4155b5c48fc2210699e5c7f033c87..e95523ff55e646e920e5a8b26e1d1402b99df894 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -23,7 +23,7 @@
(** A datatype provides useful values for types. It is a high-level API on top
of module {!Type}.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ********************************************************************** *)
(** {2 Type declarations} *)
@@ -124,12 +124,12 @@ val mem_project: 'a Type.t -> (Project_skeleton.t -> bool) -> 'a -> bool
val undefined: 'a -> 'b
(** Must be used if you don't want to implement a required function.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val identity: 'a -> 'a
(** Must be used if you want to implement a required function by [fun x ->
x]. Only useful for implementing [rehash] and [copy].
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val from_compare: 'a -> 'a -> bool
(** Must be used for [equal] in order to implement it by [compare x y = 0]
@@ -142,15 +142,15 @@ val from_pretty_code: Format.formatter -> 'a -> unit
val never_any_project: (Project_skeleton.t -> bool) -> 'a -> bool
(** Must be used for [mem_project] if values of your type does never contain
any project.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val pp_fail: Type.precedence -> Format.formatter -> 'a -> unit
(** Must be used for [internal_pretty_code] if this pretty-printer must
fail only when called.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** Sub-signature of {!S}.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module type Undefined = sig
val structural_descr: Structural_descr.t
val equal: 'a -> 'a -> bool
@@ -178,7 +178,7 @@ module Undefined: Undefined
(** Same as {!Undefined}, but the type is supposed to be marshallable by the
standard OCaml way (in particular, no hash-consing or projects inside
the type).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Serializable_undefined: Undefined
(* ********************************************************************** *)
@@ -223,7 +223,7 @@ module type Make_input = sig
end
(** Generic datatype builder.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Make(X: Make_input): S with type t = X.t
(** Additional info for building [Set], [Map] and [Hashtbl]. *)
@@ -304,17 +304,17 @@ module With_collections(X: S)(Info: Functor_info):
module Unit: S_with_collections with type t = unit
val unit: unit Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Bool: S_with_collections with type t = bool
val bool: bool Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Int: S_with_collections with type t = int
val int: int Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Int32: S_with_collections with type t = int32
val int32: int32 Type.t
@@ -330,12 +330,12 @@ val float: float Type.t
module Char: S_with_collections with type t = char
val char: char Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module String: S_with_collections with type t = string
val string: string Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Formatter: S with type t = Format.formatter
val formatter: Format.formatter Type.t
@@ -366,7 +366,7 @@ module type Polymorphic = sig
end
(** Functor for polymorphic types with only 1 type variable.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Polymorphic
(P: sig
include Type.Polymorphic_input
@@ -393,7 +393,7 @@ module type Polymorphic2 = sig
end
(** Functor for polymorphic types with 2 type variables.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Polymorphic2
(P: sig
include Type.Polymorphic2_input
@@ -428,7 +428,7 @@ end
(** Functor for polymorphic types with 3 type variables.
@since Oxygen-20120901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Polymorphic3
(P: sig
include Type.Polymorphic3_input
@@ -474,7 +474,7 @@ end
(** Functor for polymorphic types with 4 type variables.
@since Oxygen-20120901
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Polymorphic4
(P: sig
include Type.Polymorphic4_input
@@ -523,7 +523,7 @@ module Polymorphic4
module Poly_pair: Polymorphic2 with type ('a, 'b) poly = 'a * 'b
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Pair(T1: S)(T2: S): S with type t = T1.t * T2.t
module Pair_with_collections(T1: S)(T2: S)(Info: Functor_info):
S_with_collections with type t = T1.t * T2.t
@@ -531,7 +531,7 @@ val pair: 'a Type.t -> 'b Type.t -> ('a * 'b) Type.t
module Poly_ref: Polymorphic with type 'a poly = 'a ref
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Ref(T: S) : S with type t = T.t ref
val t_ref: 'a Type.t -> 'a ref Type.t
@@ -546,7 +546,7 @@ val option: 'a Type.t -> 'a option Type.t
module Poly_list: Polymorphic with type 'a poly = 'a list
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module List(T: S) : S with type t = T.t list
module List_with_collections(T:S)(Info:Functor_info):
@@ -554,7 +554,7 @@ module List_with_collections(T:S)(Info:Functor_info):
(** @since Fluorine-20130401 *)
val list: 'a Type.t -> 'a list Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Poly_array: Polymorphic with type 'a poly = 'a array
(** @since Neon-20140301 *)
@@ -593,7 +593,7 @@ module Quadruple_with_collections
(T1: S)(T2: S)(T3: S)(T4:S)(Info: Functor_info):
S_with_collections with type t = T1.t * T2.t * T3.t * T4.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Function
(T1: sig include S val label: (string * (unit -> t) option) option end)
(T2: S)
@@ -603,7 +603,7 @@ val func:
?label:string * (unit -> 'a) option -> 'a Type.t ->
'b Type.t ->
('a -> 'b) Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val optlabel_func:
string -> (unit -> 'a) -> 'a Type.t -> 'b Type.t -> ('a -> 'b) Type.t
@@ -615,7 +615,7 @@ val func2:
?label2:string * (unit -> 'b) option -> 'b Type.t ->
'c Type.t ->
('a -> 'b -> 'c) Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val func3:
?label1:string * (unit -> 'a) option -> 'a Type.t ->
@@ -623,7 +623,7 @@ val func3:
?label3:string * (unit -> 'c) option -> 'c Type.t ->
'd Type.t ->
('a -> 'b -> 'c -> 'd) Type.t
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val func4:
?label1:string * (unit -> 'a) option -> 'a Type.t ->
diff --git a/src/libraries/datatype/structural_descr.mli b/src/libraries/datatype/structural_descr.mli
index ff1106d9e5902956e1636f8bd0d578d813372021..0d5b8d69f2240a9c4a3c737ea566ccbbbabb43b4 100644
--- a/src/libraries/datatype/structural_descr.mli
+++ b/src/libraries/datatype/structural_descr.mli
@@ -58,7 +58,7 @@ type t = private
| Structure of structure
(** Provide a description of the representation of data.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| T_pack of single_pack (** Internal use only.
Do not use it outside the library *)
@@ -71,7 +71,7 @@ and structure = private
of their declarations in that type). Each element of this latter array
is an array of [t] that describes (in order) the fields of the
corresponding constructor.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Array of pack (** The data is an array of values of the same type, each
value being described by the pack. *)
@@ -82,7 +82,7 @@ and structure = private
val pack: t -> pack
(** Pack a structural descriptor in order to embed it inside another one.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val recursive_pack: recursive -> pack
(** Pack a recursive descriptor.
@@ -145,7 +145,7 @@ val p_abstract: pack
val p_unit : pack
val p_int : pack
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val p_string : pack
val p_float : pack
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index cf324f26944eb0cf20340eb7424cbb243dcd2a0f..4152f0ae302be59171469bb2b1c1d94dbe6dff2b 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -24,7 +24,7 @@
type. This API is quite low level. Prefer to use module {!Datatype} instead
whenever possible.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ****************************************************************************)
(** {2 Type declaration} *)
@@ -34,7 +34,7 @@ type 'a t
(** Type of type values. For each monomorphic type [ty], a value of type [ty
t] dynamically represents the type [ty]. Such a value is called a type
value and should be unique for each static monomorphic type.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
type 'a ty = 'a t
@@ -45,8 +45,8 @@ type 'a ty = 'a t
(** Precedences used for generating the minimal number of parenthesis in
combination with function {!par} below. *)
type precedence =
- | Basic (** @plugin development guide *)
- | Call (** @plugin development guide *)
+ | Basic (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
+ | Call (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
| Tuple
| List
| NoPar
@@ -62,7 +62,7 @@ type precedence =
let myself = Call in
par p_caller myself fmt pp]
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val par:
precedence -> precedence -> Format.formatter -> (Format.formatter -> unit) ->
unit
@@ -78,7 +78,7 @@ val par_ty_name: ('a t -> bool) -> 'a t -> string
exception AlreadyExists of string
(** May be raised by {!register}.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val register:
?closure:bool ->
@@ -103,14 +103,14 @@ exception No_abstract_type of string
(** Apply this functor to access to the abstract type of the given name.
@raise No_abstract_type if no such abstract type was registered.
@since Nitrogen-20111001
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Abstract(T: sig val name: string end): sig
type t
val ty: t ty
end
val name: 'a t -> string
-(** @plugin development name *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val structural_descr: 'a t -> Structural_descr.t
val reprs: 'a t -> 'a list
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index fd9f1db82879143f6a5c4e248924fe4124cff279..b02367b77089ed3b6a4cd3c2e87ed2b67e011071 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -27,7 +27,7 @@
possible to have many projects at the same time. For registering a new
state in the Frama-C projects, apply the functor {!State_builder.Register}.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************* *)
(** {2 Types for project} *)
@@ -67,7 +67,7 @@ exception NoProject
val current: unit -> t
(** The current project.
@raise NoProject if there is no project.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_current: t -> bool
(** Check whether the given project is the current one or not. *)
@@ -116,7 +116,7 @@ val set_current: ?on:bool -> ?selection:State_selection.t -> t -> unit
(** Set the current project with the given one.
The flag [on] is not for casual users.
@raise Invalid_argument if the given project does not exist anymore.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val register_after_set_current_hook: user_only:bool -> (t -> unit) -> unit
(** [register_after_set_current_hook f] adds a hook on function
@@ -132,7 +132,7 @@ val on: ?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b
(** [on p f x] sets the current project to [p], computes [f x] then
restores the current project. You should use this function if you use a
project different of [current ()].
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val set_keep_current: bool -> unit
(** [set_keep_current b] keeps the current project forever (even after the end
@@ -171,7 +171,7 @@ val clear: ?selection:State_selection.t -> ?project:t -> unit -> unit
(** Clear the given project. Default project is [current ()]. All the
internal states of the given project are now empty (wrt the action
registered with {!register_todo_on_clear}).
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val register_todo_before_clear: (t -> unit) -> unit
(** Register an action performed just before clearing a project.
@@ -204,7 +204,7 @@ exception IOError of string
val save: ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit
(** Save a given project in a file. Default project is [current ()].
@raise IOError if the project cannot be saved.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val load: ?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t -> t
(** Load a file into a new project given by its name.
@@ -218,7 +218,7 @@ val load: ?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t
}
@raise IOError if the project cannot be loaded
@return the new project containing the loaded data.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val save_all: ?selection:State_selection.t -> Filepath.Normalized.t -> unit
(** Save all the projects in a file.
diff --git a/src/libraries/project/project_skeleton.mli b/src/libraries/project/project_skeleton.mli
index 454b1c0d861a91732fc214dba62ee624203679f8..a651b6c5e5884647308abe2dd020be8b183b29ce 100644
--- a/src/libraries/project/project_skeleton.mli
+++ b/src/libraries/project/project_skeleton.mli
@@ -41,7 +41,7 @@ end
type t = private
{ pid: int; mutable name: string; mutable unique_name: string }
(** @since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
type project = t
(** @since Carbon-20101201 *)
diff --git a/src/libraries/project/state.mli b/src/libraries/project/state.mli
index cc8bbff434a8554900d9beb62461e2d1e2de79e4..a992a10252800811d2370a5cc733192c0ded0787 100644
--- a/src/libraries/project/state.mli
+++ b/src/libraries/project/state.mli
@@ -22,7 +22,7 @@
(** A state is a project-compliant mutable value.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Project_skeleton
@@ -100,7 +100,7 @@ val unique_name_from_name: string -> string
val dummy: t
(** A dummy state.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val dummy_unique_name: string
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index c3a630b794a3869907eeaf8819e7a541622ae9f3..a6917f55689a1b2e368ed36cdeadfb0c6cb8a823 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -24,7 +24,7 @@
Provide ways to implement signature [State_builder.S].
Depending on the builder, also provide some additional useful
information.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************* *)
(* ************************************************************************* *)
@@ -85,7 +85,7 @@ end
[Datatype] represents the datatype of a state, [Local_state]
explains how to deal with the client-side state and [Info] are additional
required information.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Register
(Datatype: Datatype.S)
(Local_state: State.Local with type t = Datatype.t)
@@ -119,7 +119,7 @@ module type Ref = sig
(** Reset the reference to its default value. *)
end
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Ref
(Data:Datatype.S)
(Info:sig
@@ -358,7 +358,7 @@ module type Hashtbl = sig
val remove: key -> unit
end
-(** @plugin development guide
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
- [H] is the hashtable implementation
- [Data] is the datatype for values stored in the table
*)
diff --git a/src/libraries/project/state_selection.mli b/src/libraries/project/state_selection.mli
index 3a97d3488988fd17848791879149d62e84ca23b5..3711690d96c8b959aaa6c38c1e7e9ae6513954d5 100644
--- a/src/libraries/project/state_selection.mli
+++ b/src/libraries/project/state_selection.mli
@@ -23,7 +23,7 @@
(** A state selection is a set of states with operations for easy handling of
state dependencies.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************** *)
(** {2 Type declarations} *)
@@ -32,7 +32,7 @@
type t
(** Type of a state selection.
@since Carbon-20101201
- @plugin development guide
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide
*)
val ty: t Type.t
@@ -85,13 +85,13 @@ val mem: t -> State.t -> bool
val with_dependencies: State.t -> t
(** The selection containing the given state and all its dependencies.
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val only_dependencies: State.t -> t
(** The selection containing all the dependencies of the given state (but not
this state itself).
@since Carbon-20101201
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val with_codependencies: State.t -> t
(** The selection containing the given state and all its co-dependencies.
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index d736864c0c471948fc67fd8160f565624b8ccdd7..984f3af72236ddcab72a779563ad827bc5c3546a 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -209,7 +209,7 @@ val the: exn:exn -> 'a option -> 'a
@raise Invalid_argument if the value is [None] and [exn] is not specified.
@return v if the value is [Some v].
@before 23.0-Vanadium [exn] was an optional argument.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val opt_hash: ('a -> int) -> 'a option -> int
(** @since Sodium-20150201 *)
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 9520988353c06d43fb3e27b64638c83a59ac0fa0..74af92e038c3750d93354fe2c302cbcaa51a7e31 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Pretty-printer utilities.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ********************************************************************** *)
(** {2 null formatters} *)
diff --git a/src/plugins/from/from_parameters.mli b/src/plugins/from/from_parameters.mli
index 6f6a9fc88e4ececd134511fa3d6334fcd8187cd4..3264710b5c2fc5c982a282f767e695652991a568 100644
--- a/src/plugins/from/from_parameters.mli
+++ b/src/plugins/from/from_parameters.mli
@@ -26,7 +26,7 @@ include Plugin.S
module ForceDeps: Parameter_sig.With_output
(** Option -calldeps.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module ForceCallDeps: Parameter_sig.With_output
(** Option -show-indirect-deps *)
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index f920b516f972b307c8ec3a04529c79c0d8dceb6a..5e18605413afa48366ddb8326f9c8d32d36cc87d 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** The extensible GUI.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
open Cil_types
@@ -82,7 +82,7 @@ class protected_menu_factory:
Gtk_helper.host -> GMenu.menu -> [ GMenu.menu ] GMenu.factory
(** This is the type of extension points for the GUI.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
class type main_window_extension_points = object
inherit view_code
@@ -158,7 +158,7 @@ class type main_window_extension_points = object
localizable.
If the button 3 is released, the first argument is popped as a
contextual menu.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
method register_source_highlighter :
(reactive_buffer -> Pretty_source.localizable ->
@@ -243,7 +243,7 @@ class main_window : unit -> main_window_extension_points
val register_extension : (main_window_extension_points -> unit) -> unit
(** Register an extension to the main GUI. It will be invoked at
initialization time.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val register_reset_extension : (main_window_extension_points -> unit) -> unit
(** Register a function to be called whenever the main GUI reset method is
diff --git a/src/plugins/gui/dgraph_helper.mli b/src/plugins/gui/dgraph_helper.mli
index a57f5fc064c3bf0f692d450434b7c868fb34a9c9..833311fd11b61e577c38c72451cc44ddf9fcdad1 100644
--- a/src/plugins/gui/dgraph_helper.mli
+++ b/src/plugins/gui/dgraph_helper.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Create a new window displaying a graph.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val graph_window:
parent: GWindow.window ->
title:string ->
diff --git a/src/plugins/pdg_types/pdgTypes.mli b/src/plugins/pdg_types/pdgTypes.mli
index e90bc536de1e7316d67addf4c4b3315a866a7426..e2d8d340a408cad0b39a93d41ce9f9c36f3575c1 100644
--- a/src/plugins/pdg_types/pdgTypes.mli
+++ b/src/plugins/pdg_types/pdgTypes.mli
@@ -22,7 +22,7 @@
(** This module defines the types that are used to store the PDG of a
function.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** [Dpd] stands for 'dependence'. This object is used as a label on the edges
* of the PDG. There are three kinds of dependencies :
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index 40f1eb7c2d98cca4f390ac3296444570ecbc268d..7dbed34009667141240597e93f6d7b7036ef55dd 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
include
Plugin.Register
@@ -30,7 +30,7 @@ include
let help = "function callees"
end)
-(** @plugin development guide *)
+(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module ForceUsers =
False
(struct
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index ae7383efe459843611c1b59a0001c1065d0f8ccc..4de2db2e4260c3232d1c6188f045884730356137 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -85,7 +85,7 @@ val compute : unit -> unit
@raise Db.Value.Incorrect_number_of_arguments if some arguments are
specified for the entry point using {!Db.Value.fun_set_args}, and
an incorrect number of them is given.
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_computed : unit -> bool
(** Return [true] iff the Eva analysis has been done. *)
diff --git a/src/plugins/value_types/cilE.mli b/src/plugins/value_types/cilE.mli
index a32fc59c506ef02be93f94870f4b9d21428b44e9..595aa7782e3301ee72337cc6776ed001eec6a04e 100644
--- a/src/plugins/value_types/cilE.mli
+++ b/src/plugins/value_types/cilE.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Value analysis alarms
- @plugin development guide *)
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(* ************************************************************************* *)
(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis