From 739cf415c096337ef1e02e041ffa4baad8b4861a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 26 Sep 2024 15:14:51 +0200
Subject: [PATCH] [doc] Update doc, use alert for handlers
---
src/kernel_services/ast_data/cil_types.ml | 4 +---
.../ast_printing/cil_printer.mli | 4 ++++
.../ast_queries/acsl_extension.ml | 1 +
src/kernel_services/ast_queries/ast_diff.mli | 6 +++++-
src/kernel_services/ast_queries/cil.mli | 4 +++-
src/kernel_services/ast_queries/logic_env.mli | 21 +++++++++++++++----
.../ast_queries/logic_typing.mli | 6 ++++--
7 files changed, 35 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 49c18c4fd5..3c0114a585 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1691,7 +1691,7 @@ and spec = {
and acsl_extension = {
ext_id : int;
ext_name : string;
- ext_plugin : string; (** @since Frama-C+dev *)
+ ext_plugin : string; (** @since Frama-C+dev *)
ext_loc : location;
ext_has_status : bool;
ext_kind : acsl_extension_kind
@@ -1809,8 +1809,6 @@ and global_annotation =
* attributes * location
(** associated terms, reading function, writing function *)
| Daxiomatic of string * global_annotation list * attributes * location
- (** last option is the external loader(name, plugin) responsible for the
- module importer *)
| Dmodule of
string * global_annotation list * attributes * loader option * location
| Dtype of logic_type_info * location (** declaration of a logic type. *)
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index c329765d0c..0576e14f7d 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -80,7 +80,11 @@ val set_extension_handler:
(** Used to setup a reference related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this.
@since 21.0-Scandium
+ @before Frama-C+dev functions did not take a [plugin:string] parameter
*)
+[@@alert acsl_extension_handler
+ "This function can only be called by Acsl_extension"]
+
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index ee109a99b5..f53f18f354 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -386,3 +386,4 @@ let () =
~short_print:Extensions.short_print;
Ast_diff.set_extension_diff
~is_same_ext: Extensions.is_same_ext
+[@@alert "-acsl_extension_handler"]
diff --git a/src/kernel_services/ast_queries/ast_diff.mli b/src/kernel_services/ast_queries/ast_diff.mli
index 919b490c4c..ec38c8c201 100644
--- a/src/kernel_services/ast_queries/ast_diff.mli
+++ b/src/kernel_services/ast_queries/ast_diff.mli
@@ -128,12 +128,16 @@ val is_same_term: term -> term -> is_same_env -> bool
val is_same_predicate: predicate -> predicate -> is_same_env -> bool
-(** access custom comparison functions for ACSL extensions *)
val set_extension_diff:
is_same_ext:
(plugin:string -> string ->
acsl_extension_kind -> acsl_extension_kind -> is_same_env -> bool)
-> unit
+(** access custom comparison functions for ACSL extensions
+ @before Frama-C+dev This function did not take a [plugin:string] parameter
+*)
+[@@alert acsl_extension_handler
+ "This function can only be called by Acsl_extension"]
(** performs a comparison of AST between the current and the original
project, which must have been set beforehand.
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 317703668b..89ed0c7b2e 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2469,9 +2469,11 @@ val set_extension_handler:
acsl_extension_kind visitAction) ->
unit
(** Used to setup a reference related to the handling of ACSL extensions.
- If your name is not [Acsl_extension], do not call this
@since 21.0-Scandium
+ @before Frama-C+dev This function did not take a [plugin:string] parameter
*)
+[@@alert acsl_extension_handler
+ "This function can only be called by Acsl_extension"]
(** void
@deprecated Frama-C+dev *)
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index c45551e9d4..02706a7aa0 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -67,10 +67,20 @@ val preprocess_extension_block:
plugin:string -> string -> string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list
-(** Return the plugin name of the ACSL extension *)
+(** Return the plugin name of the ACSL extension. If [plugin] is [None], we try
+ to find an extension with this [name] in our tables (can crash in case of
+ ambiguity), if it is [Some] we check that this extension exists.
+ @before Frama-C+dev The [plugin] parameter did not exist and the function
+ only performed the [None] case.
+*)
val extension_from : ?plugin:string -> string -> string
-(** Return the plugin name of the module importer extension *)
+(** Return the plugin name of the module importer extension. If [plugin] is
+ [None], we try to find an extension with this [name] in our tables (can
+ crash in case of ambiguity), if it is [Some] we check that this extension
+ exists.
+ @since Frama-C+dev
+*)
val importer_from : ?plugin:string -> string -> string
(** {2 Global Tables} *)
@@ -269,9 +279,12 @@ val set_extension_handler:
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this.
@since 21.0-Scandium
- @before Frama-C+dev functions did not take a [plugin] parameter.
- [get_plugins], [is_importer] and [importer_from] did not exist
+ @before Frama-C+dev functions did not take a [plugin:string] parameter.
+ [get_plugins], [is_importer] and [importer_from] did not exist, and
+ [extension_from] did not take an optional plugin parameter.
*)
+[@@alert acsl_extension_handler
+ "This function can only be called by Acsl_extension"]
val init_dependencies: State.t -> unit
(** Used to postpone dependency of Lenv global tables wrt Cil_state, which
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e1d6c76350..431c9a9605 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -322,10 +322,12 @@ val set_extension_handler:
string list -> unit) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
- If your name is not [Acsl_extension], do not call this
@since 21.0-Scandium
- @before Frama-C+dev functions did not take a [plugin] parameter
+ @before Frama-C+dev functions did not take a [plugin:string] parameter and
+ the function [importer] did not exists.
*)
+[@@alert acsl_extension_handler
+ "This function can only be called by Acsl_extension"]
(** Type the given extension.
@before Frama-C+dev the function took one less argument, [plugin], which is
--
GitLab