From 35e0680718ded1bac4267966224d5076aba655e7 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 25 Sep 2024 17:25:03 +0200
Subject: [PATCH] [kernel] Remove all plugin options
- Always print plugin except kernel
- The only optional plugin is used in extension_from and plugin_from
- All other acsl_extension functions take a plugin:string
- these functions raise Not_found is the extension is not registered
- can also fatal in case of ambiguity if plugin is None
---
src/kernel_internals/parsing/logic_lexer.mll | 50 ++++++----
src/kernel_internals/parsing/logic_parser.mly | 9 +-
src/kernel_internals/typing/cabs2cil.ml | 6 --
src/kernel_internals/typing/unfold_loops.ml | 2 +-
src/kernel_services/ast_data/cil_types.ml | 4 +-
.../ast_printing/cil_printer.ml | 9 +-
.../ast_printing/cil_printer.mli | 4 +-
.../ast_printing/cil_types_debug.ml | 10 +-
.../ast_printing/logic_print.ml | 27 ++----
.../ast_queries/acsl_extension.ml | 97 +++++++++----------
.../ast_queries/acsl_extension.mli | 2 +-
src/kernel_services/ast_queries/ast_diff.mli | 2 +-
src/kernel_services/ast_queries/cil.mli | 2 +-
src/kernel_services/ast_queries/filecheck.ml | 5 -
.../ast_queries/logic_const.mli | 2 +-
src/kernel_services/ast_queries/logic_env.ml | 19 ++--
src/kernel_services/ast_queries/logic_env.mli | 45 ++++-----
.../ast_queries/logic_typing.ml | 6 +-
.../ast_queries/logic_typing.mli | 14 +--
.../ast_queries/logic_utils.ml | 1 -
src/kernel_services/parsetree/logic_ptree.ml | 8 +-
src/plugins/eva/utils/eva_annotations.ml | 3 +-
tests/spec/Extend_errors.ml | 4 +-
tests/spec/oracle/import.0.res.oracle | 2 +-
tests/spec/oracle/import.1.res.oracle | 15 +--
25 files changed, 167 insertions(+), 181 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 2c9bc770ce3..312584cdd23 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -103,6 +103,38 @@
let c = Utf8_logic.from_unichar !code in
find_utf8 c
+ let extension ~plugin name =
+ try
+ (* extension_from will raise Not_found or fatal, if extension does not
+ exist or if there are ambiguities between extension names and the
+ plugin is not provided. *)
+ let plugin = Logic_env.extension_from ?plugin name in
+ match Logic_env.extension_category ~plugin name with
+ | Cil_types.Ext_contract -> Some (EXT_CONTRACT (name, plugin))
+ | Cil_types.Ext_global ->
+ if Logic_env.is_extension_block ~plugin name
+ then Some (EXT_GLOBAL_BLOCK (name, plugin))
+ else Some (EXT_GLOBAL (name, plugin))
+ | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT (name, plugin))
+ with Not_found ->
+ (* We need to distinguish here which token was parsed (with or without
+ plugin) to help the parser (cf. ext_loader rule). *)
+ match plugin with
+ | None ->
+ begin
+ try
+ (* importer_from will raise Not_found or fatal, if extension does not
+ exist or if there are ambiguities between extension names and the
+ plugin is not provided. *)
+ let plugin = Logic_env.importer_from name in
+ Some (EXT_LOADER (name, plugin))
+ with Not_found -> None
+ end
+ | Some plugin ->
+ if Logic_env.is_importer ~plugin name then
+ Some (EXT_LOADER_PLUGIN (name, plugin))
+ else None
+
let identifier, is_acsl_keyword =
let all_kw = Hashtbl.create 37 in
let type_kw = Hashtbl.create 3 in
@@ -188,23 +220,7 @@
(Hashtbl.find all_kw s)
loc
with Not_found ->
- let res =
- match Logic_env.extension_category ~plugin s with
- | exception Not_found ->
- begin
- match Logic_env.is_importer ~plugin s, plugin with
- | false, _ -> None
- | true, None -> Some (EXT_LOADER s)
- | true, Some _ -> Some (EXT_LOADER_PLUGIN (s, plugin))
- end
- | Cil_types.Ext_contract -> Some (EXT_CONTRACT (s, plugin))
- | Cil_types.Ext_global ->
- if Logic_env.is_extension_block ~plugin s
- then Some (EXT_GLOBAL_BLOCK (s, plugin))
- else Some (EXT_GLOBAL (s, plugin))
- | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT (s, plugin))
- in
- match res with
+ match extension ~plugin s with
| None ->
if Logic_env.typename_status s then TYPENAME s
else
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 200a6e7c85c..08a045b18ce 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -290,8 +290,7 @@
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
%token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
%token ADMIT_ENSURES ADMIT_EXITS ADMIT_CONTINUES ADMIT_BREAKS ADMIT_RETURNS
-%token <string> EXT_LOADER
-%token <string * string option> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT EXT_LOADER_PLUGIN
+%token <string * string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT EXT_LOADER EXT_LOADER_PLUGIN
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
%token LOGIC PREDICATE INDUCTIVE AXIOM LEMMA LBRACE RBRACE
@@ -953,7 +952,7 @@ full_identifier:
| id = EXT_CONTRACT { fst id }
| id = EXT_GLOBAL { fst id }
| id = EXT_GLOBAL_BLOCK { fst id }
-| id = EXT_LOADER { id }
+| id = EXT_LOADER { fst id }
| id = EXT_LOADER_PLUGIN { fst id }
| id = IDENTIFIER_EXT { id }
| id = IDENTIFIER_LOADER { id }
@@ -1726,7 +1725,7 @@ ext_loader:
"Ignoring unregistered module importer extension '%s'" $1;
raise Unknown_ext
}
-| EXT_LOADER COLON { $1, None }
+| EXT_LOADER COLON { $1 }
| EXT_LOADER_PLUGIN { $1 }
| IDENTIFIER_LOADER { raise Unknown_ext }
@@ -1997,7 +1996,7 @@ is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { fst $1 }
| EXT_GLOBAL { fst $1 }
| EXT_GLOBAL_BLOCK { fst $1 }
-| EXT_LOADER { $1 }
+| EXT_LOADER { fst $1 }
| EXT_LOADER_PLUGIN { fst $1 }
| IDENTIFIER_EXT { $1 }
| IDENTIFIER_LOADER { $1 }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index afa7e0d92b3..d9929b8846d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9823,12 +9823,6 @@ and doBody local_env (blk: Cabs.block) : chunk =
(Logic_ptree.AExtended(_,is_loop,(name,plugin,_)),loc) ->
let source = fst loc in
(match Logic_env.extension_category ~plugin name, is_loop with
- | exception Not_found ->
- Kernel.(
- warning
- ~source ~wkey:wkey_acsl_extension
- "%s is not a known extension" name);
- [], false
| Ext_code_annot Ext_here, false -> [], false
| Ext_code_annot Ext_next_stmt, false -> [], true
| Ext_code_annot Ext_next_loop, true -> [], false
diff --git a/src/kernel_internals/typing/unfold_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
index 7c4a4943d71..f54d801c0d7 100644
--- a/src/kernel_internals/typing/unfold_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -696,7 +696,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
Logic_const.tinteger number
] in
let ext =
- Logic_const.new_acsl_extension ~plugin:(Some "kernel") "unfold" loc
+ Logic_const.new_acsl_extension ~plugin:"kernel" "unfold" loc
false kind
in
let annot =Logic_const.new_code_annotation (AExtended([],true,ext)) in
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index bfbda226787..488707721d9 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 option; (** @since Frama-C+dev *)
+ ext_plugin : string; (** @since Frama-C+dev *)
ext_loc : location;
ext_has_status : bool;
ext_kind : acsl_extension_kind
@@ -1802,7 +1802,7 @@ and global_annotation =
(** associated terms, reading function, writing function *)
| Daxiomatic of string * global_annotation list * attributes * location
(** last option is the external loader responsible for the module importer *)
- | Dmodule of string * global_annotation list * attributes * (string * string option) option * location
+ | Dmodule of string * global_annotation list * attributes * (string * string) option * location
| Dtype of logic_type_info * location (** declaration of a logic type. *)
| Dlemma of
string * logic_label list * string list *
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6728f8aedff..c2468724ed7 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3285,12 +3285,9 @@ class cil_printer () = object (self)
(self#logic_type (Some print_decl)) mfi.mi_field_type
method private pp_loader fmt (name, plugin) =
- match plugin with
- | None -> pp_print_string fmt name
- | Some plugin ->
- if Datatype.String.equal plugin "kernel"
- then pp_print_string fmt name
- else fprintf fmt "\\%s::%s" plugin name
+ if Datatype.String.equal plugin "kernel"
+ then pp_print_string fmt name
+ else fprintf fmt "\\%s::%s" plugin name
method global_annotation fmt = function
| Dtype_annot (a,_) ->
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index d97b732662c..c329765d0c3 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -72,9 +72,9 @@ val print_global: Cil_types.global -> bool
(**/**)
val set_extension_handler:
- print:(plugin:string option -> string -> Printer_api.extensible_printer_type ->
+ print:(plugin:string -> string -> Printer_api.extensible_printer_type ->
Format.formatter -> Cil_types.acsl_extension_kind -> unit) ->
- short_print:(plugin:string option -> string -> Printer_api.extensible_printer_type ->
+ short_print:(plugin:string -> string -> Printer_api.extensible_printer_type ->
Format.formatter -> Cil_types.acsl_extension_kind -> unit) ->
unit
(** Used to setup a reference related to the handling of ACSL extensions.
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 9533be029c0..e44d426765a 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -899,9 +899,9 @@ and pp_spec fmt spec =
and pp_acsl_extension fmt ext =
Format.fprintf fmt
- "{ext_id=%d;ext_name=%s;ext_loc=%a;ext_has_status=%B;ext_kind=%a}"
- ext.ext_id ext.ext_name pp_location ext.ext_loc ext.ext_has_status
- pp_acsl_extension_kind ext.ext_kind
+ "{ext_id=%d; ext_name=%s; ext_plugin=%s; ext_loc=%a; ext_has_status=%B; ext_kind=%a}"
+ ext.ext_id ext.ext_name ext.ext_plugin pp_location ext.ext_loc
+ ext.ext_has_status pp_acsl_extension_kind ext.ext_kind
and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
@@ -973,9 +973,9 @@ and pp_global_annotation fmt = function
pp_attributes attributes pp_location location
| Dmodule(string,global_annotation_list,attributes,loader,location) ->
let pp_loader fmt (name, plugin) =
- Format.fprintf fmt "(%s, %a)" name (pp_option pp_string) plugin
+ Format.fprintf fmt "(%s, %s)" name plugin
in
- Format.fprintf fmt "Dmodule(%a,%a,%a,%a,%a)" pp_string string
+ Format.fprintf fmt "Dmodule(%a,%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
pp_attributes attributes
(pp_option pp_loader) loader
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 63e590b6e12..acbddebd63d 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -310,21 +310,20 @@ let print_model_annot fmt ty =
(print_logic_type None) ty.model_type
ty.model_name
-let print_plugin_ext fmt (plugin,name) =
- match plugin with
- | None -> pp_print_string fmt name
- | Some "kernel" -> pp_print_string fmt name
- | Some plugin -> fprintf fmt "\\%s::%s" plugin name
+let print_plugin fmt (plugin, name) =
+ if Datatype.String.equal plugin "kernel"
+ then pp_print_string fmt name
+ else fprintf fmt "\\%s::%s" plugin name
let rec print_extended_decl fmt d =
let aux fmt d = print_extended_decl fmt d.extended_node in
match d with
| Ext_lexpr(name, plugin, d) ->
fprintf fmt "@[<2>%a@ %a@]"
- print_plugin_ext (plugin,name) (pp_list ~sep:",@ " print_lexpr) d
+ print_plugin (plugin,name) (pp_list ~sep:",@ " print_lexpr) d
| Ext_extension(name, plugin, id,d) ->
fprintf fmt "@[<2>%a@ %s@ {@\n%a@]@\n}"
- print_plugin_ext (plugin,name) id (pp_list ~sep:"@\n" aux) d
+ print_plugin (plugin,name) id (pp_list ~sep:"@\n" aux) d
let rec print_decl fmt d =
match d.decl_node with
@@ -383,16 +382,8 @@ let rec print_decl fmt d =
fprintf fmt "@[<2>module@ %s@ {@\n%a@]@\n}" name
(pp_list ~sep:"@\n" print_decl) ds
| LDimport (loader,mId,asId) ->
- let pp_loader fmt (name, plugin) =
- match plugin with
- | None -> pp_print_string fmt name
- | Some plugin ->
- if Datatype.String.equal plugin "kernel"
- then pp_print_string fmt name
- else fprintf fmt "\\%s::%s" plugin name
- in
fprintf fmt "@[<2>import" ;
- Option.iter (fprintf fmt "%a:" pp_loader) loader ;
+ Option.iter (fprintf fmt "%a:" print_plugin) loader ;
fprintf fmt "@ %s" mId ;
Option.iter (fprintf fmt "@ \\as %s") asId ;
fprintf fmt ";@]@\n}"
@@ -474,8 +465,8 @@ let print_spec fmt spec =
spec.spec_disjoint_behaviors
let print_extension fmt (name, plugin, ext) =
- fprintf fmt "%a %a"
- print_plugin_ext (plugin,name) (pp_list ~sep:",@ " print_lexpr) ext
+ fprintf fmt "%a %a" print_plugin (plugin,name)
+ (pp_list ~sep:",@ " print_lexpr) ext
let print_code_annot fmt ca =
let print_behaviors fmt bhvs =
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index a288005b958..03370128e86 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -172,50 +172,26 @@ module Extensions = struct
(* [get_plugin] is a getter to access the [plugin] field from extension_*
types, to keep this function generic. *)
- let mem ~get_plugin tbl ~plugin name =
- match Hashtbl.find_opt tbl name, plugin with
- (* Extension is not registered. *)
- | None, _ -> false
- (* We do not remove extensions from this table, and always add an element
- the first time a key is registered, so this case cannot happen. *)
- | Some [], _ -> assert false
- (* One extension registered, no ambiguity. *)
- | Some [_], None -> true
- (* One extension registered, make sure the plugin field matches. *)
- | Some [e], Some plugin -> String.equal plugin (get_plugin e)
+ let mem_gen ~get_plugin tbl ~plugin name =
+ match Hashtbl.find_opt tbl name with
+ | None -> false
+ | Some [] -> assert false
+ | Some [e] -> String.equal plugin (get_plugin e)
(* Ambiguity on name, look for an extension with the right plugin. *)
- | Some l, Some plugin ->
- List.exists (fun e -> String.equal plugin (get_plugin e)) l
- (* Ambiguity on name without providing plugin name. *)
- | Some l, None -> throw_ambiguity_error ~get_plugin name l
-
- (* [get_plugin] is a getter to access the [plugin] field from extension_*
- types, to keep this function generic. Can raise Not_found. *)
- let find ~get_plugin tbl ~plugin name =
- match Hashtbl.find tbl name, plugin with
- (* We do not remove extensions from this table, and always add an element
- the first time a key is registered, so this case cannot happen. *)
- | [], _ -> assert false
- (* One extension registered, no ambiguity. *)
- | [e], None -> e
- (* One extension registered, make sure the plugin field matches. *)
- | [e], Some plugin ->
- if String.equal plugin (get_plugin e) then e else raise Not_found
- (* Ambiguity on name, look for an extension with the right plugin. *)
- | l, Some plugin ->
- List.find (fun e -> String.equal plugin (get_plugin e)) l
- (* Ambiguity on name without providing plugin name. *)
- | l, None -> throw_ambiguity_error ~get_plugin name l
+ | Some l -> List.exists (fun e -> String.equal plugin (get_plugin e)) l
(* Generic function for find functions, catch Not_found and throw a fatal
- instead. *)
+ instead. [get_plugin] is a getter to access the [plugin] field from
+ extension_* types, to keep this function generic. *)
let find_gen ~get_plugin data tbl ~plugin name =
- try find ~get_plugin ~plugin tbl name
+ try
+ match Hashtbl.find tbl name with
+ | [] -> assert false
+ | [e] -> if String.equal plugin (get_plugin e) then e else raise Not_found
+ | l -> List.find (fun e -> String.equal plugin (get_plugin e)) l
with Not_found ->
- Kernel.fatal ~current:true "Unsupported %s extension named '%a%s'"
- data
- (Pretty_utils.pp_opt ~pre:"\\" ~suf:"::" Format.pp_print_string) plugin
- name
+ Kernel.fatal ~current:true "Unsupported %s extension named '\\%s::%s'"
+ data plugin name
let get_plugin_common (e : extension_common) = e.plugin
@@ -235,20 +211,17 @@ module Extensions = struct
find_gen ~get_plugin:get_plugin_block "clause" ext_block_tbl
let find_importer =
- find_gen ~get_plugin:get_plugin_importer "importer" ext_importer_tbl
+ find_gen ~get_plugin:get_plugin_importer "module importer" ext_importer_tbl
- (* [Logic_lexer] can ask for something that is not a category, which is not
- a fatal error so we do not caught the Not_found exception. *)
- let category ~plugin name =
- (find ~get_plugin:get_plugin_common ext_tbl ~plugin name).category
+ let category ~plugin name = (find_common ~plugin name).category
let importer ~plugin name = (find_importer ~plugin name).importer
- let is_extension = mem ~get_plugin:get_plugin_common ext_tbl
+ let is_extension = mem_gen ~get_plugin:get_plugin_common ext_tbl
- let is_extension_block = mem ~get_plugin:get_plugin_block ext_block_tbl
+ let is_extension_block = mem_gen ~get_plugin:get_plugin_block ext_block_tbl
- let is_importer = mem ~get_plugin:get_plugin_importer ext_importer_tbl
+ let is_importer = mem_gen ~get_plugin:get_plugin_importer ext_importer_tbl
let fullname plugin name =
if Datatype.String.equal plugin "kernel"
@@ -263,13 +236,13 @@ module Extensions = struct
make ~plugin name cat ?preprocessor typer
?visitor ?printer ?short_printer ?is_same_ext status
in
- if is_extension ~plugin:(Some "kernel") name then
+ if is_extension ~plugin:"kernel" name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register ACSL extension %s reserved by frama-c. \
Rename this extension to avoid conflict with the kernel. Ignored \
extension" name
else begin
- if is_extension ~plugin:(Some plugin) name then
+ if is_extension ~plugin name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register ACSL extension %s twice with plugin %s. \
Ignoring the second extension"
@@ -287,13 +260,13 @@ module Extensions = struct
let register_module_importer ~plugin name importer =
Kernel.debug ~dkey:Kernel.dkey_acsl_extension
"Registering module importer extension %s" (fullname plugin name);
- if is_importer ~plugin:(Some "kernel") name then
+ if is_importer ~plugin:"kernel" name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register module importer extension %s reserved by frama-c. \
Rename to avoid conflict with the kernel. Ignored module importer" name
else
begin
- if is_importer ~plugin:(Some plugin) name then
+ if is_importer ~plugin name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register module importer extension %s twice with plugin \
%s. Ignoring the second extension" name plugin
@@ -350,6 +323,24 @@ module Extensions = struct
let is_same_ext ~plugin name ext1 ext2 =
let is_same = (find_common ~plugin name).is_same_ext in
is_same ext1 ext2
+
+ let find_plugin ~get_plugin tbl ~plugin name =
+ match plugin with
+ | Some plugin ->
+ if mem_gen ~get_plugin tbl ~plugin name then plugin
+ else raise Not_found
+ | None ->
+ match Hashtbl.find_opt tbl name with
+ | None -> raise Not_found
+ | Some [] -> assert false
+ | Some [e] -> get_plugin e
+ | Some l -> throw_ambiguity_error ~get_plugin name l
+
+ let extension_from ?plugin name =
+ find_plugin ~get_plugin:get_plugin_common ext_tbl ~plugin name
+
+ let importer_from ?plugin name =
+ find_plugin ~get_plugin:get_plugin_importer ext_importer_tbl ~plugin name
end
(* Registration functions *)
@@ -380,7 +371,9 @@ let () =
~is_importer:Extensions.is_importer
~preprocess: Extensions.preprocess
~is_extension_block: Extensions.is_extension_block
- ~preprocess_block: Extensions.preprocess_block;
+ ~preprocess_block: Extensions.preprocess_block
+ ~extension_from: Extensions.extension_from
+ ~importer_from: Extensions.importer_from;
Logic_typing.set_extension_handler
~is_extension: Extensions.is_extension
~typer: Extensions.typing
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index ba981fb9e2b..9655516725c 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -128,7 +128,7 @@ type register_extension =
(** same as {!register_extension}, but for extensions that parse an axiomatic
block, resulting in a {!Cil_types.Ext_annot}. *)
type register_extension_block =
- plugin: string -> string ->
+ plugin:string -> string ->
?preprocessor:extension_preprocessor_block -> extension_typer_block ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer ->
diff --git a/src/kernel_services/ast_queries/ast_diff.mli b/src/kernel_services/ast_queries/ast_diff.mli
index 1905bde1d55..919b490c4c4 100644
--- a/src/kernel_services/ast_queries/ast_diff.mli
+++ b/src/kernel_services/ast_queries/ast_diff.mli
@@ -131,7 +131,7 @@ 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 option -> string ->
+ (plugin:string -> string ->
acsl_extension_kind -> acsl_extension_kind -> is_same_env -> bool)
-> unit
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index a7dc3b33e4b..317703668b8 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2465,7 +2465,7 @@ val pp_from_ref: (Format.formatter -> from -> unit) ref
val pp_behavior_ref: (Format.formatter -> behavior -> unit) ref
val set_extension_handler:
- visit:(plugin:string option -> string -> cilVisitor -> acsl_extension_kind ->
+ visit:(plugin:string -> string -> cilVisitor -> acsl_extension_kind ->
acsl_extension_kind visitAction) ->
unit
(** Used to setup a reference related to the handling of ACSL extensions.
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 1d8ba991ead..30ece109efa 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -622,11 +622,6 @@ module Base_checker = struct
match ca.annot_content with
| AExtended (_, is_loop, {ext_name; ext_plugin}) ->
(match Logic_env.extension_category ~plugin:ext_plugin ext_name, is_loop with
- | exception Not_found ->
- Kernel.(
- warning ~wkey:wkey_acsl_extension
- "%s is not a known extension" ext_name);
- my_labels
| Ext_code_annot (Ext_next_stmt | Ext_next_both), false ->
Logic_const.post_label :: my_labels
| Ext_code_annot Ext_here, false -> my_labels
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 32baab0045a..bf69aa11aca 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -70,7 +70,7 @@ val new_predicate: ?kind:predicate_kind -> predicate -> identified_predicate
@before the function took one less argument, [~plugin] which is now
used to set the [ext_plugin] field.
*)
-val new_acsl_extension: plugin:string option -> string -> location -> bool ->
+val new_acsl_extension: plugin:string -> 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_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 50bfcfb14b0..e525918905a 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -32,9 +32,11 @@ module Extensions = struct
let ref_preprocess = ref (fun ~plugin:_ _ -> assert false)
let ref_is_extension_block = ref (fun ~plugin:_ _ -> assert false)
let ref_preprocess_block = ref (fun ~plugin:_ _ -> assert false)
+ let ref_extension_from = ref (fun ?plugin:_ _ -> assert false)
+ let ref_importer_from = ref (fun ?plugin:_ _ -> assert false)
let set_extension_handler ~category ~is_extension ~is_importer ~preprocess
- ~is_extension_block ~preprocess_block =
+ ~is_extension_block ~preprocess_block ~extension_from ~importer_from =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_is_importer := is_importer ;
@@ -42,6 +44,8 @@ module Extensions = struct
ref_preprocess := preprocess ;
ref_is_extension_block := is_extension_block;
ref_preprocess_block := preprocess_block;
+ ref_extension_from := extension_from;
+ ref_importer_from := importer_from;
initialized := true ;
()
@@ -51,7 +55,10 @@ module Extensions = struct
let category ~plugin name = !ref_category ~plugin name
let preprocess ~plugin name = !ref_preprocess ~plugin name
let preprocess_block ~plugin name = !ref_preprocess_block ~plugin name
+ let extension_from ?plugin name = !ref_extension_from ?plugin name
+ let importer_from ?plugin name = !ref_importer_from ?plugin name
end
+
let set_extension_handler = Extensions.set_extension_handler
let is_extension = Extensions.is_extension
let is_extension_block = Extensions.is_extension_block
@@ -59,6 +66,8 @@ let is_importer = Extensions.is_importer
let extension_category = Extensions.category
let preprocess_extension = Extensions.preprocess
let preprocess_extension_block = Extensions.preprocess_block
+let extension_from = Extensions.extension_from
+let importer_from = Extensions.importer_from
let error (b,_e) fstring =
Kernel.abort
@@ -161,7 +170,7 @@ module ModuleOccurence =
(Datatype.Option
(Datatype.Pair
(Datatype.String) (* external loader name *)
- (Datatype.Option(Datatype.String)))) (* external loader plugin *)
+ (Datatype.String))) (* external loader plugin *)
(Cil_datatype.Location)
module Modules =
@@ -416,9 +425,3 @@ let iter_builtin_logic_function f =
Logic_builtin.iter (fun _ info -> List.iter f info)
let iter_builtin_logic_type f = Logic_type_builtin.iter (fun _ info -> f info)
let iter_builtin_logic_ctor f = Logic_ctor_builtin.iter (fun _ info -> f info)
-
-(*
- Local Variables:
- compile-command: "make -C ../../.."
- End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index d6188b73f14..c45551e9d48 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -32,31 +32,31 @@ open Cil_types
@before Frama-C+def the function took one less argument, [plugin], which is
now used to avoid ambiguity if plugins use the same name for an extension
*)
-val is_extension: plugin:string option -> string -> bool
+val is_extension: plugin:string -> string -> bool
(** Return [true] if an extension block is registered for the given plugin.
@before Frama-C+def the function took one less argument, [plugin], which is
now used to avoid ambiguity if plugins use the same name for an extension
*)
-val is_extension_block: plugin:string option -> string -> bool
+val is_extension_block: plugin:string -> string -> bool
(** Return [true] if a module importer is registered for the given name and
plugin. @since Frama-C+dev
*)
-val is_importer: plugin:string option -> string -> bool
+val is_importer: plugin:string -> string -> bool
(** Return the extension category.
@raise Not_Found if the extension is not registered
@before Frama-C+def the function took one less argument, [plugin], which is
now used to avoid ambiguity if plugins use the same name for an extension
*)
-val extension_category: plugin:string option -> string -> ext_category
+val extension_category: plugin:string -> string -> ext_category
(** Return the extension preprocessor.
@before Frama-C+def the function took one less argument, [plugin], which is
now used to avoid ambiguity if plugins use the same name for an extension
*)
-val preprocess_extension: plugin:string option -> string ->
+val preprocess_extension: plugin:string -> string ->
Logic_ptree.lexpr list -> Logic_ptree.lexpr list
(** Return the extension block preprocessor.
@@ -64,9 +64,15 @@ val preprocess_extension: plugin:string option -> string ->
now used to avoid ambiguity if plugins use the same name for an extension
*)
val preprocess_extension_block:
- plugin:string option -> string -> string * Logic_ptree.extended_decl list ->
+ plugin:string -> string -> string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list
+(** Return the plugin name of the ACSL extension *)
+val extension_from : ?plugin:string -> string -> string
+
+(** Return the plugin name of the module importer extension *)
+val importer_from : ?plugin:string -> string -> string
+
(** {2 Global Tables} *)
module Logic_info: State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_info list
@@ -93,7 +99,7 @@ module Axiomatics: State_builder.Hashtbl
module Modules: State_builder.Hashtbl
with type key = string
(* loader (name, plugin), location *)
- and type data = (string * string option) option * Cil_types.location
+ and type data = (string * string) option * Cil_types.location
val builtin_states: State.t list
@@ -248,30 +254,25 @@ val builtin_types_as_typenames: unit -> unit
(** {2 Internal use} *)
val set_extension_handler:
- category:(plugin:string option -> string -> ext_category) ->
- is_extension:(plugin:string option -> string -> bool) ->
- is_importer:(plugin:string option -> string -> bool) ->
- preprocess:
- (plugin:string option -> string -> Logic_ptree.lexpr list ->
- Logic_ptree.lexpr list) ->
- is_extension_block:(plugin:string option -> string -> bool) ->
+ category:(plugin:string -> string -> ext_category) ->
+ is_extension:(plugin:string -> string -> bool) ->
+ is_importer:(plugin:string -> string -> bool) ->
+ preprocess: (plugin:string -> string -> Logic_ptree.lexpr list ->
+ Logic_ptree.lexpr list) ->
+ is_extension_block:(plugin:string -> string -> bool) ->
preprocess_block:
- (plugin:string option -> string -> string * Logic_ptree.extended_decl list ->
+ (plugin:string -> string -> string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list) ->
+ extension_from:(?plugin:string -> string -> string) ->
+ importer_from:(?plugin:string -> string -> string) ->
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.
- [get_plugins] and [is_importer] did not exist
+ [get_plugins], [is_importer] and [importer_from] did not exist
*)
val init_dependencies: State.t -> unit
(** Used to postpone dependency of Lenv global tables wrt Cil_state, which
is initialized afterwards. *)
-
-(*
- Local Variables:
- compile-command: "make -C ../../.."
- End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index dac950c3f04..525a5e7b2d8 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4340,10 +4340,8 @@ struct
| Some (name', plugin'), oldloc ->
if plugin <> plugin' || name <> name' then
C.error loc
- "Module %s already imported with loader %a%s (at %a)"
- id
- (Pretty_utils.pp_opt ~pre:"\\" ~suf:"::" Format.pp_print_string) plugin'
- name'
+ "Module %s already imported with loader \\%s::%s (at %a)"
+ id plugin' name'
Cil_printer.pp_location oldloc
else None
| exception Not_found ->
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 86976720d3f..e1d6c763509 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -312,13 +312,13 @@ val post_state_env: termination_kind -> logic_type -> Lenv.t
(** {2 Internal use} *)
val set_extension_handler:
- is_extension:(plugin:string option -> string -> bool) ->
- typer: (plugin:string option -> string -> typing_context -> location ->
+ is_extension:(plugin:string -> string -> bool) ->
+ typer: (plugin:string -> string -> typing_context -> location ->
Logic_ptree.lexpr list -> (bool * acsl_extension_kind)) ->
- typer_block:(plugin:string option -> string -> typing_context -> location ->
+ typer_block:(plugin:string -> string -> typing_context -> location ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind) ->
- importer: (plugin:string option -> string -> module_builder -> location ->
+ importer: (plugin:string -> string -> module_builder -> location ->
string list -> unit) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
@@ -332,7 +332,7 @@ val set_extension_handler:
now used to avoid ambiguity if plugins use the same name for an extension
*)
val get_typer :
- plugin:string option ->
+ plugin:string ->
string ->
typing_context:typing_context ->
loc:location ->
@@ -343,7 +343,7 @@ val get_typer :
now used to avoid ambiguity if plugins use the same name for an extension
*)
val get_typer_block:
- plugin:string option ->
+ plugin:string ->
string ->
typing_context:typing_context ->
loc:Logic_ptree.location ->
@@ -354,7 +354,7 @@ val get_typer_block:
@since Frama-C+dev
*)
val get_importer:
- plugin:string option ->
+ plugin:string ->
string ->
builder:module_builder ->
loc:Logic_ptree.location ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 9981b48d505..ecadf4ba6ed 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -722,7 +722,6 @@ let is_annot_next_stmt c =
"%s is not a code annotation extension" ext_name)
in
(match Logic_env.extension_category ~plugin:ext_plugin ext_name with
- | exception Not_found -> warn_not_a_code_annot () ; false
| Ext_code_annot (Ext_here | Ext_next_loop)-> false
| Ext_code_annot Ext_next_stmt-> true
| Ext_code_annot Ext_next_both-> not is_loop
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 1f3a3e07f14..2315b025d2c 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -168,7 +168,7 @@ type toplevel_predicate =
(** ACSL extension.
@before Frama-C+dev Was of type [string * lexpr list].
*)
-type extension = string * string option * lexpr list
+type extension = string * string * lexpr list
(** type invariant. *)
type type_annot = {inv_name: string;
@@ -250,7 +250,7 @@ and decl_node =
| LDmodule of string * decl list
(** [LDmodule(id,decls)]
represents a module of axiomatic definitions.*)
- | LDimport of (string * string option) option * string * string option
+ | LDimport of (string * string) option * string * string option
(** [LDimport(loader,module,alias)]
imports symbols from module using the specified loader,
with optional alias.*)
@@ -288,10 +288,10 @@ and variant = lexpr * string option
(** Global ACSL extension. *)
and global_extension =
- | Ext_lexpr of string * string option * lexpr list
+ | Ext_lexpr of string * string * lexpr list
(** @before Frama-C+dev Was of type [string * lexpr list]. *)
- | Ext_extension of string * string option * string * extended_decl list
+ | Ext_extension of string * string * string * extended_decl list
(** @before Frama-C+dev Was of type [string * string * extended_decl list]. *)
and extended_decl = {
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index 4ed203a7404..d00ff4fd282 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -114,9 +114,8 @@ struct
let add ~emitter stmt annot =
let loc = Cil_datatype.Stmt.loc stmt in
let param = M.export annot in
- let plugin = Some "eva" in
let extension =
- Logic_const.new_acsl_extension ~plugin name loc false param
+ Logic_const.new_acsl_extension ~plugin:"eva" 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_errors.ml b/tests/spec/Extend_errors.ml
index 9a4d583747e..5e747ae035a 100644
--- a/tests/spec/Extend_errors.ml
+++ b/tests/spec/Extend_errors.ml
@@ -32,8 +32,8 @@ let catch msg f x =
with _ -> ()
let cover_errors () =
- catch "User Error" (Logic_env.is_extension ~plugin:None) "foo";
- catch "Unsupported" (Logic_env.preprocess_extension ~plugin:(Some "myplugin1")) "bar"
+ catch "User Error" Logic_env.extension_from "foo";
+ catch "Unsupported" (Logic_env.preprocess_extension ~plugin:"myplugin1") "bar"
let cover_warnings () =
Acsl_extension.register_behavior ~plugin:"myplugin1" "foo" type_foo false;
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
index 24d4b89ebd6..1388d33b8e2 100644
--- a/tests/spec/oracle/import.0.res.oracle
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -36,7 +36,7 @@
*/
/*@ predicate check5(X::t x) = X::check(x, 0);
*/
-/*@ import bar: X::Y \as _ ;
+/*@ import \myplugin1::bar: X::Y \as _ ;
*/
/*@ predicate check6(X::Y::t x) = X::Y::check(x, 0);
*/
diff --git a/tests/spec/oracle/import.1.res.oracle b/tests/spec/oracle/import.1.res.oracle
index 7d1dfd239e1..c9118f11b16 100644
--- a/tests/spec/oracle/import.1.res.oracle
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -49,13 +49,14 @@ module A::B {
*/
/*@ predicate check5(X::t x) = X::check(x, 0);
*/
-/*@ // import bar:
- module X::Y {
- type t;
-
- predicate check(t x, ℤ k) ;
-
- }
+/*@
+// import \myplugin1::bar:
+module X::Y {
+ type t;
+
+ predicate check(t x, ℤ k) ;
+
+ }
*/
/*@ predicate check6(X::Y::t x) = X::Y::check(x, 0);
*/
--
GitLab