From 01a58bddc8605b5476759e59b957cc756a2bce15 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 24 Sep 2024 14:42:37 +0200
Subject: [PATCH] [kernel] Name plugin parameter when registering extensions
---
src/kernel_internals/typing/unfold_loops.ml | 5 ++++-
src/kernel_services/ast_queries/cil.ml | 4 ++--
src/kernel_services/ast_queries/logic_const.ml | 2 +-
src/kernel_services/ast_queries/logic_const.mli | 4 ++--
src/kernel_services/ast_queries/logic_typing.ml | 8 ++++----
src/plugins/eva/utils/eva_annotations.ml | 2 +-
tests/spec/Extend_recursive_preprocess.ml | 4 ++--
7 files changed, 16 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/typing/unfold_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
index db3d6da4d5b..7c4a4943d71 100644
--- a/src/kernel_internals/typing/unfold_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -695,7 +695,10 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
(Logic_const.term (TConst (LStr "done")) (Ctype Cil_const.charPtrType)) ;
Logic_const.tinteger number
] in
- let ext = Logic_const.new_acsl_extension "unfold" (Some "kernel") loc false kind in
+ let ext =
+ Logic_const.new_acsl_extension ~plugin:(Some "kernel") "unfold" loc
+ false kind
+ in
let annot =Logic_const.new_code_annotation (AExtended([],true,ext)) in
Annotations.add_code_annot
Emitter.end_user ~kf:(Option.get self#current_kf) sloop annot;
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index fe3a350ce80..f67e99e8860 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1794,8 +1794,8 @@ and visitCilExtended vis orig =
let visit = Extensions.visit orig.ext_name in
let e' = doVisitCil vis id (visit ~plugin:orig.ext_plugin vis) childrenCilExtended orig.ext_kind in
if Visitor_behavior.is_fresh vis#behavior then
- Logic_const.new_acsl_extension orig.ext_name orig.ext_plugin orig.ext_loc
- orig.ext_has_status e'
+ Logic_const.new_acsl_extension ~plugin:orig.ext_plugin orig.ext_name
+ orig.ext_loc orig.ext_has_status e'
else if orig.ext_kind == e' then orig else {orig with ext_kind = e'}
and childrenCilExtended vis p =
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 2e52b0fdd74..91f440b76c3 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -58,7 +58,7 @@ let refresh_predicate p = { p with ip_id = PredicateId.next () }
let new_identified_term t =
{ it_id = TermId.next (); it_content = t }
-let new_acsl_extension ext_name ext_plugin ext_loc ext_has_status ext_kind = {
+let new_acsl_extension ~plugin:ext_plugin ext_name ext_loc ext_has_status ext_kind = {
ext_id = ExtendedId.next ();
ext_name;
ext_plugin;
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 9de783d0643..32baab0045a 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -67,10 +67,10 @@ val new_predicate: ?kind:predicate_kind -> predicate -> identified_predicate
(** creates a new acsl_extension with a fresh id.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
@since Chlorine-20180501
- @begore the function took one less argument, [string option] which is now
+ @before the function took one less argument, [~plugin] which is now
used to set the [ext_plugin] field.
*)
-val new_acsl_extension: string -> string option -> location -> bool ->
+val new_acsl_extension: plugin:string option -> string -> location -> bool ->
acsl_extension_kind -> acsl_extension
(** Gives a new id to an existing predicate.
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 6d56d016a25..dac950c3f04 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3790,7 +3790,7 @@ struct
in
if Extensions.is_extension ~plugin name then
let status , kind = Extensions.typer name ~plugin ~typing_context ~loc ps in
- Logic_const.new_acsl_extension name plugin loc status kind
+ Logic_const.new_acsl_extension ~plugin name loc status kind
else
C.error
loc "No type-checking function registered for extension %s" name
@@ -4502,8 +4502,8 @@ struct
| LDextended (Ext_lexpr(name, plugin, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
- let status,tcontent = Extensions.typer name ~plugin ~typing_context ~loc content in
- let textended = Logic_const.new_acsl_extension name plugin loc status tcontent in
+ let status,tcontent = Extensions.typer ~plugin name ~typing_context ~loc content in
+ let textended = Logic_const.new_acsl_extension ~plugin name loc status tcontent in
Some (Dextended (textended, [], loc))
| LDextended (Ext_extension (name, plugin, kind, content)) ->
@@ -4511,7 +4511,7 @@ struct
let status,tcontent =
Extensions.typer_block name ~plugin ~typing_context ~loc (kind,content)
in
- let textended = Logic_const.new_acsl_extension name plugin loc status tcontent in
+ let textended = Logic_const.new_acsl_extension ~plugin name loc status tcontent in
Some (Dextended (textended, [], loc))
let annot = C.on_error
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index 0823af80570..4ed203a7404 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -116,7 +116,7 @@ struct
let param = M.export annot in
let plugin = Some "eva" in
let extension =
- Logic_const.new_acsl_extension name plugin loc false param
+ Logic_const.new_acsl_extension ~plugin name loc false param
in
let annot_node = Cil_types.AExtended ([], kind = Loop, extension) in
let code_annotation = Logic_const.new_code_annotation annot_node in
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index be862c32953..a4a0b4bf026 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -14,10 +14,10 @@ let ext_typing_block typing_context loc_here node =
match node.extended_node with
| Ext_lexpr (name,plugin,data) ->
let status,kind = Logic_typing.get_typer ~plugin name ~typing_context ~loc:node.extended_loc data in
- Logic_const.new_acsl_extension name plugin loc_here status kind
+ Logic_const.new_acsl_extension ~plugin name loc_here status kind
| Ext_extension (name, plugin, id, data) ->
let status,kind = Logic_typing.get_typer_block ~plugin name ~typing_context ~loc:node.extended_loc (id,data) in
- Logic_const.new_acsl_extension name plugin loc_here status kind
+ Logic_const.new_acsl_extension ~plugin name loc_here status kind
let ext_typing_foo typing_context loc (s,d) =
let block = List.map (ext_typing_block typing_context loc) d in
--
GitLab