From 1e5c280c9ac784a31d44bf00a2df738348ee09f5 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 3 Dec 2021 17:57:28 +0100
Subject: [PATCH] [doc] add @plugin development guide annotation where they
were missing
---
src/kernel_internals/runtime/boot.mli | 3 +--
src/kernel_services/analysis/dataflow2.mli | 5 ++++-
src/kernel_services/ast_data/cil_types.mli | 1 +
src/kernel_services/ast_queries/logic_utils.mli | 1 +
src/kernel_services/cmdline_parameters/typed_parameter.mli | 5 ++++-
src/kernel_services/plugin_entry_points/log.mli | 7 ++++++-
src/kernel_services/visitors/visitor_behavior.mli | 3 +++
src/libraries/datatype/datatype.mli | 1 +
src/plugins/gui/dgraph_helper.mli | 5 +++++
9 files changed, 26 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index 0eec6c94475..11d608fcace 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 904542fe9b1..25f8da8cedf 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 7a437cc8369..506f932eaf8 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 ef79c06f510..c12b050d8a0 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 55534d22829..605be08c5c4 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 72740f68e89..5dce8e57a5a 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 6aaee136c66..5003c108ff7 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 a05da5610ad..3b6fd5ccc61 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 a57f5fc064c..0dac7a9dc8a 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:
--
GitLab