diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index 0eec6c94475dfe38885d819b1510bc5b1f20aceb..11d608fcaced570e6d4586bd475b091c177a9b77 100644
--- a/src/kernel_internals/runtime/boot.mli
+++ b/src/kernel_internals/runtime/boot.mli
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-(** Nothing is exported.
-
+(** Main entry point of Frama-C. Nothing is exported.
@plugin development guide
*)
diff --git a/src/kernel_services/analysis/dataflow2.mli b/src/kernel_services/analysis/dataflow2.mli
index 904542fe9b18f29fc1b2147120ff892c18b1c4e4..25f8da8cedf699d3ed2fddb5afb828d5b36b26f2 100644
--- a/src/kernel_services/analysis/dataflow2.mli
+++ b/src/kernel_services/analysis/dataflow2.mli
@@ -20,8 +20,11 @@
(* *)
(**************************************************************************)
-(** Implementation of data flow analyses over user-supplied domains. *)
+(** Implementation of data flow analyses over user-supplied domains.
+ @plugin development guide
+*)
+(** possible kinds of action for backward analysis *)
type 't action =
Default (** The default action *)
| Done of 't (** Do not do the default action. Use this result *)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 7a437cc8369bb26691a9a2cbe8551ad9a0d86ca5..506f932eaf850a6177fd089494b9da91b74e1ea9 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1681,6 +1681,7 @@ and ext_category =
| Ext_global
| Ext_code_annot of ext_code_annot_context
+(** @plugin development guide *)
and ext_code_annot_context =
| Ext_here (** at current program point. *)
| Ext_next_stmt (** covers next statement. *)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index ef79c06f510414ea50d57d1a24f4484cea12a90a..c12b050d8a0776b6157a92af8c104e35d1f6387e 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -180,6 +180,7 @@ val expr_to_term : ?coerce:bool -> exp -> term
[expr_to_predicate] instead.
@modify 21.0-Scandium
+ @plugin development guide
*)
val expr_to_predicate: exp -> predicate
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.mli b/src/kernel_services/cmdline_parameters/typed_parameter.mli
index 55534d228298066cd472566b8a1e307be19bc511..605be08c5c4c771cd6080bdaccae7e7971931b95 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.mli
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.mli
@@ -23,8 +23,11 @@
(** Parameter settable through a command line option.
This is a low level API, internally used by the kernel. As a plug-in
developer, you certainly prefer to use the API of {!Plugin} instead.
- @since Nitrogen-20111001 *)
+ @since Nitrogen-20111001
+ @plugin development guide
+*)
+(** generic accessor type *)
type ('a, 'b) gen_accessor =
{ get: unit -> 'a;
set: 'a -> unit;
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 72740f68e89e8842d5fa7b6c60ae5b4246d12f93..5dce8e57a5a491535c8267915b14de2d8325c406 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -135,6 +135,7 @@ module type Messages = sig
type warn_category
(** Same as above, but for warnings
@since Chlorine-20180501
+ @plugin development guide
*)
val verbose_atleast : int -> bool
@@ -267,7 +268,9 @@ module type Messages = sig
In case the [wkey] is considered as a [Failure], the continution is not called.
This kind of message denotes a fatal error aborting Frama-C.
Notice that the [~emitwith] action is called iff a message is logged.
- @since 18.0-Argon *)
+ @since 18.0-Argon
+ @plugin development guide
+ *)
val register : kind -> (event -> unit) -> unit
(** Local registry for listeners. *)
@@ -343,6 +346,7 @@ module type Messages = sig
*)
val register_warn_category: string -> warn_category
+ (** @plugin development guide *)
val is_warn_category: string -> bool
@@ -362,6 +366,7 @@ module type Messages = sig
val get_all_warn_categories_status: unit -> (warn_category * warn_status) list
val set_warn_status: warn_category -> warn_status -> unit
+ (** @plugin development guide *)
val get_warn_status: warn_category -> warn_status
diff --git a/src/kernel_services/visitors/visitor_behavior.mli b/src/kernel_services/visitors/visitor_behavior.mli
index 6aaee136c669b736fb1e21130f5bb6ab24db913e..5003c108ff773e3372c3a694777941ca6b2a3fb4 100644
--- a/src/kernel_services/visitors/visitor_behavior.mli
+++ b/src/kernel_services/visitors/visitor_behavior.mli
@@ -99,12 +99,14 @@ module type Get = sig
val enumitem: t -> enumitem -> enumitem
val typeinfo: t -> typeinfo -> typeinfo
val stmt: t -> stmt -> stmt
+ (** @plugin development guide *)
val logic_info: t -> logic_info -> logic_info
val logic_type_info: t -> logic_type_info -> logic_type_info
val fieldinfo: t -> fieldinfo -> fieldinfo
val model_info: t -> model_info -> model_info
val logic_var: t -> logic_var -> logic_var
val kernel_function: t -> kernel_function -> kernel_function
+ (** @plugin development guide *)
val fundec: t -> fundec -> fundec
end
@@ -187,6 +189,7 @@ module Set: Set
{!Cil_types.varinfo}: [Set_orig.varinfo vis vi new_original_repr].
@since 20.0-Calcium
+ @plugin development guide
*)
module Set_orig: Set
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index a05da5610adf6c89533d382de06848907db2a85e..3b6fd5ccc615f2927c0408bedbcb8f818aa27235 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -290,6 +290,7 @@ end
module type S_with_collections = sig
include S
module Set: Set with type elt = t
+ (** @plugin development guide *)
module Map: Map with type key = t
module Hashtbl: Hashtbl with type key = t
(** @plugin development guide *)
diff --git a/src/plugins/gui/dgraph_helper.mli b/src/plugins/gui/dgraph_helper.mli
index a57f5fc064c3bf0f692d450434b7c868fb34a9c9..0dac7a9dc8a9e9f0b59e0e004c7f63a22957d4ed 100644
--- a/src/plugins/gui/dgraph_helper.mli
+++ b/src/plugins/gui/dgraph_helper.mli
@@ -20,6 +20,11 @@
(* *)
(**************************************************************************)
+(** Creation of windows for displaying graphs. Only available
+ for lablgtk2. In lablgtk3 mode, the window will only display a
+ text saying that the feature is not available.
+*)
+
(** Create a new window displaying a graph.
@plugin development guide *)
val graph_window: