From f5684b07069add69b75e65b12e544cedb5425e4b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 17 May 2022 10:32:05 +0200
Subject: [PATCH] [doc] @plugin -> @see
---
src/init/boot/boot.ml | 2 +-
src/kernel_internals/typing/cabs2cil.mli | 2 +-
src/kernel_internals/typing/frontc.mli | 2 +-
.../abstract_interp/abstract_interp.mli | 2 +-
.../abstract_interp/lattice_type.ml | 2 +-
src/kernel_services/abstract_interp/lmap.mli | 2 +-
.../abstract_interp/lmap_bitwise.mli | 2 +-
.../abstract_interp/locations.mli | 14 ++--
src/kernel_services/ast_data/annotations.mli | 8 +--
src/kernel_services/ast_data/ast.mli | 10 +--
src/kernel_services/ast_data/cil_types.ml | 72 +++++++++----------
src/kernel_services/ast_data/globals.mli | 6 +-
.../ast_data/kernel_function.mli | 8 +--
src/kernel_services/ast_data/property.mli | 2 +-
.../ast_data/property_status.mli | 2 +-
.../ast_queries/acsl_extension.mli | 14 ++--
src/kernel_services/ast_queries/cil.mli | 70 +++++++++---------
.../ast_queries/cil_datatype.mli | 4 +-
.../ast_queries/cil_state_builder.mli | 4 +-
src/kernel_services/ast_queries/file.mli | 20 +++---
.../ast_queries/logic_const.ml | 6 +-
.../ast_queries/logic_const.mli | 6 +-
.../ast_queries/logic_typing.mli | 2 +-
.../ast_queries/logic_utils.mli | 4 +-
.../cmdline_parameters/cmdline.mli | 34 ++++-----
.../parameter_customize.mli | 4 +-
.../cmdline_parameters/parameter_sig.ml | 24 +++----
.../cmdline_parameters/parameter_state.mli | 2 +-
src/kernel_services/parsetree/cabs.ml | 4 +-
.../plugin_entry_points/db.mli | 20 +++---
.../plugin_entry_points/dynamic.mli | 10 +--
.../plugin_entry_points/emitter.mli | 2 +-
.../plugin_entry_points/journal.mli | 2 +-
.../plugin_entry_points/kernel.mli | 10 +--
.../plugin_entry_points/log.mli | 38 +++++-----
.../plugin_entry_points/plugin.mli | 6 +-
src/kernel_services/visitors/visitor.ml | 2 +-
src/kernel_services/visitors/visitor.mli | 14 ++--
.../visitors/visitor_behavior.mli | 16 ++---
src/libraries/datatype/datatype.mli | 56 +++++++--------
src/libraries/datatype/structural_descr.mli | 8 +--
src/libraries/datatype/type.mli | 16 ++---
src/libraries/project/project.mli | 14 ++--
src/libraries/project/project_skeleton.mli | 2 +-
src/libraries/project/state.mli | 4 +-
src/libraries/project/state_builder.mli | 8 +--
src/libraries/project/state_selection.mli | 8 +--
src/libraries/stdlib/extlib.mli | 2 +-
src/libraries/utils/pretty_utils.mli | 2 +-
src/plugins/from/from_parameters.mli | 2 +-
src/plugins/gui/design.mli | 8 +--
src/plugins/gui/dgraph_helper.mli | 2 +-
src/plugins/pdg_types/pdgTypes.mli | 2 +-
src/plugins/users/users_register.ml | 4 +-
src/plugins/value/engine/analysis.mli | 2 +-
src/plugins/value_types/cilE.mli | 2 +-
56 files changed, 298 insertions(+), 298 deletions(-)
diff --git a/src/init/boot/boot.ml b/src/init/boot/boot.ml
index 0140f5cb6c5..db11a81677a 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 09f58c88463..21b11001345 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 5204f0ae738..2bd29fab1e4 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 e86e3d65532..0269a087479 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 f5e0608d520..79c2456447e 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 20e1d5f5990..61069f42fce 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 fc44a814aa1..8551bf7244f 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 e071ac4420f..c76b6002c11 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 485a8c2c3b6..81e0911b96c 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 b8fbba2777c..4667c234bba 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 5e3bd30bf63..9071268fc3b 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 fe2b181766a..2ae3a939ec7 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 0c954057a43..ce21b069f5d 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 eaf6c8bc0db..af54a56f572 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 3252bc6eaf5..bbe2f162668 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 a651c98bf1f..6b581a5ec04 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 ac92bae3b7c..d673ff60b03 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 807648fbb37..db708394580 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 516ac23c060..cd5240d4ac9 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 8042cf4420e..10473c5178b 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 8b003070708..459a8569510 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 2a7d97c98f4..5bbc7457d3e 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 4eebe17c00c..7784937d3ab 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 307d889ee9b..a7ea2707d7e 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 d335b4e10dd..420e6b58ef5 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 2d2d03cc876..f29dad1f049 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 b5558a5aa42..e032660b655 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 aabe1efd6e2..8051e561be0 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 5313481fd20..309a515159c 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 0c37f844ea0..e254132ee26 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 070fc655970..2dcdd083b7a 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 0da83cb0b71..96e4ae157d5 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 f9be3ee7a31..33fb39a20b8 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 b58ecaa79ad..ee8a7b424fc 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 a44b6b4ae22..9a83010ddc7 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 0851fea0859..227209f8525 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 cbfdfbc2c3f..2319f037679 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 8469257aaf4..1413219ed84 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 9e4adf0201f..c395d1d848b 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 fb520585b8f..e95523ff55e 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 ff1106d9e59..0d5b8d69f22 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 cf324f26944..4152f0ae302 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 fd9f1db8287..b02367b7708 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 454b1c0d861..a651b6c5e58 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 cc8bbff434a..a992a102528 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 c3a630b794a..a6917f55689 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 3a97d348898..3711690d96c 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 d736864c0c4..984f3af7223 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 9520988353c..74af92e038c 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 6f6a9fc88e4..3264710b5c2 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 f920b516f97..5e18605413a 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 a57f5fc064c..833311fd11b 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 e90bc536de1..e2d8d340a40 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 40f1eb7c2d9..7dbed340096 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 ae7383efe45..4de2db2e426 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 a32fc59c506..595aa7782e3 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
--
GitLab