diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 08a045b18ce952a9142cf81e8acecc4d9e110d5c..01d7509c06f6d75a7962b12a604c1143980ea032 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -259,6 +259,23 @@
let cv_ghost = Attr("ghost", [])
let toplevel_pred tp_kind tp_statement = { tp_kind; tp_statement }
+
+ let extension ext_name ext_plugin ext_content =
+ {ext_name; ext_plugin; ext_content}
+
+ let global_extension gext_name gext_plugin gext_kind gext_content =
+ Ext_extension {gext_name; gext_plugin; gext_kind; gext_content}
+
+ let import loader module_name module_alias =
+ let import_loader =
+ match loader with
+ | None -> None
+ | Some (loader_name, loader_plugin) ->
+ Some {loader_name;loader_plugin}
+ in
+ LDimport { import_loader; module_name; module_alias}
+
+
%}
/*****************************************************************************/
@@ -1258,7 +1275,8 @@ ne_simple_clauses:
{ let allocation,assigns,post_cond,extended = snd $4 in
let name, plugin = $1 in
let processed = Logic_env.preprocess_extension ~plugin name $2 in
- allocation,assigns,post_cond,(name, plugin, processed)::extended
+ let ext = extension name plugin processed in
+ allocation,assigns,post_cond,ext::extended
}
| post_cond_kind lexpr clause_kw { missing $loc($2) ";" $3 }
| allocation clause_kw { missing $loc($1) ";" $2 }
@@ -1478,21 +1496,21 @@ loop_variant:
loop_grammar_extension:
| LOOP EXT_CODE_ANNOT extension_content SEMICOLON {
let open Cil_types in
- let ext, plugin = $2 in
+ let name, plugin = $2 in
try
- begin match Logic_env.extension_category ~plugin ext with
+ begin match Logic_env.extension_category ~plugin name with
| Ext_code_annot (Ext_next_loop | Ext_next_both) ->
- let processed = Logic_env.preprocess_extension ~plugin ext $3 in
- (ext, plugin, processed)
+ let processed = Logic_env.preprocess_extension ~plugin name $3 in
+ {ext_name = name; ext_plugin = plugin; ext_content = processed}
| Ext_code_annot (Ext_here | Ext_next_stmt) ->
raise
(Not_well_formed
- (loc $loc($2), ext ^ " is not a loop annotation extension"))
+ (loc $loc($2), name ^ " is not a loop annotation extension"))
| _ -> raise Not_found
end
with Not_found ->
Kernel.fatal ~source:(pos $startpos($2))
- "%s is not a code annotation extension. Parser got wrong lexeme." ext
+ "%s is not a code annotation extension. Parser got wrong lexeme." name
}
;
@@ -1527,12 +1545,13 @@ code_annotation:
| EXT_CODE_ANNOT extension_content SEMICOLON
{ fun bhvs ->
let open Cil_types in
- let ext, plugin = $1 in
+ let name, plugin = $1 in
try
- begin match Logic_env.extension_category ~plugin ext with
+ begin match Logic_env.extension_category ~plugin name with
| Ext_code_annot (Ext_here | Ext_next_stmt | Ext_next_both) ->
- let processed = Logic_env.preprocess_extension ~plugin ext $2 in
- Logic_ptree.AExtended(bhvs,false,(ext,plugin,processed))
+ let processed = Logic_env.preprocess_extension ~plugin name $2 in
+ let ext = extension name plugin processed in
+ Logic_ptree.AExtended(bhvs,false,ext)
| Ext_code_annot Ext_next_loop ->
raise
(Not_well_formed
@@ -1540,12 +1559,12 @@ code_annotation:
Printf.sprintf
"%s is a loop annotation extension. It can't be used as a \
plain code annotation extension. Did you mean 'loop %s'?"
- ext ext))
+ name name))
| _ -> raise Not_found
end
with Not_found ->
Kernel.fatal ~source:(pos $startpos($1))
- "%s is not a code annotation extension. Parser got wrong lexeme" ext
+ "%s is not a code annotation extension. Parser got wrong lexeme" name
}
;
@@ -1571,14 +1590,15 @@ ext_decl:
| EXT_GLOBAL extension_content SEMICOLON {
let name, plugin = $1 in
let processed = Logic_env.preprocess_extension ~plugin name $2 in
- Ext_lexpr(name, plugin, processed)
+ let ext = extension name plugin processed in
+ Ext_lexpr ext
}
| EXT_GLOBAL_BLOCK any_identifier LBRACE ext_decls RBRACE {
let name, plugin = $1 in
let processed_id,processed_block =
Logic_env.preprocess_extension_block ~plugin name ($2,$4)
in
- Ext_extension(name, plugin, processed_id, processed_block)
+ global_extension name plugin processed_id processed_block
}
;
@@ -1695,13 +1715,13 @@ logic_def:
| MODULE push_module_name LBRACE logic_decls RBRACE
{ pop_module_types () ; LDmodule($2,$4) }
| IMPORT mId = module_name SEMICOLON
- { LDimport(None,mId,None) }
+ { import None mId None }
| IMPORT mId = module_name AS id = IDENTIFIER SEMICOLON
- { LDimport(None,mId,Some id) }
+ { import None mId (Some id) }
| IMPORT loader = ext_loader mId = module_name SEMICOLON
- { LDimport(Some loader,mId,None) }
+ { import (Some loader) mId None }
| IMPORT loader = ext_loader mId = module_name AS id = IDENTIFIER SEMICOLON
- { LDimport(Some loader,mId,Some id) }
+ { import (Some loader) mId (Some id) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
{ let (id,tvars) = $2 in
exit_type_variables_scope ();
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index d9929b8846d32ed14dec027c0d5dd88ff43503b2..4d639ed255a09ae499690bfd07c50c50d7c8e2e9 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9820,9 +9820,12 @@ and doBody local_env (blk: Cabs.block) : chunk =
s.Logic_ptree.spec_behavior,
true
| CODE_ANNOT
- (Logic_ptree.AExtended(_,is_loop,(name,plugin,_)),loc) ->
+ (Logic_ptree.AExtended(_,is_loop,ext),loc) ->
let source = fst loc in
- (match Logic_env.extension_category ~plugin name, is_loop with
+ let kind =
+ Logic_env.extension_category ~plugin:ext.ext_plugin ext.ext_name
+ in
+ (match kind, is_loop with
| Ext_code_annot Ext_here, false -> [], false
| Ext_code_annot Ext_next_stmt, false -> [], true
| Ext_code_annot Ext_next_loop, true -> [], false
@@ -9832,20 +9835,20 @@ and doBody local_env (blk: Cabs.block) : chunk =
warning
~source ~wkey:wkey_acsl_extension
"%s is a code annotation extension, \
- but used here as a loop annotation" name);
+ but used here as a loop annotation" ext.ext_name);
[], false
| Ext_code_annot Ext_next_loop, false ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
"%s is a loop annotation extension, \
- but used here as a code annotation" name);
+ but used here as a code annotation" ext.ext_name);
[], false
| (Ext_global | Ext_contract), _ ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
- "%s is not a code annotation extension" name);
+ "%s is not a code annotation extension" ext.ext_name);
[], false)
| _ -> [], false
in
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 488707721d9c36e48739e793b315a7b49001df71..49c18c4fd529f876c026412d2a7c6ebd5e5db20f 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1793,6 +1793,14 @@ and code_annotation = {
(** behavior of a function. *)
and funbehavior = behavior
+(** loader type used by Dmodules.
+ @since Frama-c+dev
+*)
+and loader = {
+ loader_name: string;
+ loader_plugin: string;
+}
+
(** global annotations, not attached to a statement or a function. *)
and global_annotation =
| Dfun_or_pred of logic_info * location
@@ -1801,8 +1809,10 @@ 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 responsible for the module importer *)
- | Dmodule of string * global_annotation list * attributes * (string * string) option * 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. *)
| 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 c2468724ed7c9421679d5b4d59c7214663e60bce..fc7d05c72804a2d36f0dbf0c858ef8de51dd3097 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3284,10 +3284,10 @@ class cil_printer () = object (self)
(self#typ None) mfi.mi_base_type
(self#logic_type (Some print_decl)) mfi.mi_field_type
- method private pp_loader fmt (name, plugin) =
- if Datatype.String.equal plugin "kernel"
- then pp_print_string fmt name
- else fprintf fmt "\\%s::%s" plugin name
+ method private pp_loader fmt loader =
+ if Datatype.String.equal loader.loader_plugin "kernel"
+ then pp_print_string fmt loader.loader_name
+ else fprintf fmt "\\%s::%s" loader.loader_plugin loader.loader_name
method global_annotation fmt = function
| Dtype_annot (a,_) ->
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index e44d426765ac4ddb4fc5c900634df1ef83c7c46a..4a1ae03abc0409845ad9d794b96efe4fc24b9f85 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -972,8 +972,8 @@ and pp_global_annotation fmt = function
(pp_list pp_global_annotation) global_annotation_list
pp_attributes attributes pp_location location
| Dmodule(string,global_annotation_list,attributes,loader,location) ->
- let pp_loader fmt (name, plugin) =
- Format.fprintf fmt "(%s, %s)" name plugin
+ let pp_loader fmt loader =
+ Format.fprintf fmt "(%s, %s)" loader.loader_name loader.loader_plugin
in
Format.fprintf fmt "Dmodule(%a,%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index acbddebd63d65a1971b586b8c9bfcb50429189bc..91bbf80e966b1defd19735cf112733140c021122 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -310,7 +310,7 @@ let print_model_annot fmt ty =
(print_logic_type None) ty.model_type
ty.model_name
-let print_plugin fmt (plugin, name) =
+let print_plugin fmt (name, plugin) =
if Datatype.String.equal plugin "kernel"
then pp_print_string fmt name
else fprintf fmt "\\%s::%s" plugin name
@@ -318,12 +318,15 @@ let print_plugin fmt (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) ->
+ | Ext_lexpr ext ->
fprintf fmt "@[<2>%a@ %a@]"
- print_plugin (plugin,name) (pp_list ~sep:",@ " print_lexpr) d
- | Ext_extension(name, plugin, id,d) ->
+ print_plugin (ext.ext_name, ext.ext_plugin)
+ (pp_list ~sep:",@ " print_lexpr) ext.ext_content
+ | Ext_extension ext ->
fprintf fmt "@[<2>%a@ %s@ {@\n%a@]@\n}"
- print_plugin (plugin,name) id (pp_list ~sep:"@\n" aux) d
+ print_plugin (ext.gext_name, ext.gext_plugin)
+ ext.gext_kind
+ (pp_list ~sep:"@\n" aux) ext.gext_content
let rec print_decl fmt d =
match d.decl_node with
@@ -381,11 +384,14 @@ let rec print_decl fmt d =
| LDmodule (name,ds) ->
fprintf fmt "@[<2>module@ %s@ {@\n%a@]@\n}" name
(pp_list ~sep:"@\n" print_decl) ds
- | LDimport (loader,mId,asId) ->
+ | LDimport import ->
fprintf fmt "@[<2>import" ;
- Option.iter (fprintf fmt "%a:" print_plugin) loader ;
- fprintf fmt "@ %s" mId ;
- Option.iter (fprintf fmt "@ \\as %s") asId ;
+ Option.iter (fun loader ->
+ let name, plugin = loader.loader_name, loader.loader_plugin in
+ fprintf fmt "%a:" print_plugin (name, plugin)
+ ) import.import_loader ;
+ fprintf fmt "@ %s" import.module_name ;
+ Option.iter (fprintf fmt "@ \\as %s") import.module_alias ;
fprintf fmt ";@]@\n}"
| LDinvariant (s,e) ->
fprintf fmt "@[<2>invariant@ %s:@ %a;@]" s print_lexpr e
@@ -464,9 +470,9 @@ let print_spec fmt spec =
~sep:"@\n" ~suf:"@\n" (pp_list ~sep:",@ " pp_print_string))
spec.spec_disjoint_behaviors
-let print_extension fmt (name, plugin, ext) =
- fprintf fmt "%a %a" print_plugin (plugin,name)
- (pp_list ~sep:",@ " print_lexpr) ext
+let print_extension fmt ext =
+ fprintf fmt "%a %a" print_plugin (ext.ext_name, ext.ext_plugin)
+ (pp_list ~sep:",@ " print_lexpr) ext.ext_content
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 03370128e86f0c135ded36f7b6680c05375c7f8d..ee109a99b5c7be8ef73069da84cb111c726672d5 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -278,7 +278,7 @@ module Extensions = struct
let preprocess_block ~plugin name = (find_block ~plugin name).preprocessor
- let typing_gen ~status ~typer name typing_context loc es =
+ let typing_gen ~typer ~status name typing_context loc es =
let normal_error = ref false in
let has_error _ = normal_error := true in
let wrapper =
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 525a5e7b2d8bc8cd415c9bf129cebe6b266decac..69cb0cb35c6ff584a0287e04eea2b79cdf7a8f68 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3783,17 +3783,20 @@ struct
old_behaviors
behaviors
- let type_extended ~typing_context ~loc (name, plugin, ps) =
- let loc = match ps with
+ let type_extended ~typing_context ~loc {ext_name; ext_plugin; ext_content} =
+ let loc = match ext_content with
| [] -> loc
| p::_ -> p.lexpr_loc
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 ~plugin name loc status kind
+ if Extensions.is_extension ~plugin:ext_plugin ext_name then
+ let status , kind =
+ Extensions.typer ext_name ~plugin:ext_plugin ~typing_context ~loc
+ ext_content
+ in
+ Logic_const.new_acsl_extension ~plugin:ext_plugin ext_name loc status kind
else
C.error
- loc "No type-checking function registered for extension %s" name
+ loc "No type-checking function registered for extension %s" ext_name
(* This module is used to sort the list of behaviors in [complete] and
[disjoint] clauses, in order to remove duplicate clauses. *)
@@ -3996,7 +3999,8 @@ struct
let env = loop_annot_env () in
let ctxt = base_ctxt env in
Cil_types.AAssigns(behav, type_assign ctxt ~accept_formal:true env a)
- | AExtended (behav, is_loop, (name, plugin, _ as ext)) ->
+ | AExtended (behav, is_loop, ext) ->
+ let name, plugin = ext.ext_name, ext.ext_plugin in
let kind = Logic_env.extension_category ~plugin name in
let pre_state, post_state =
match kind,is_loop with
@@ -4327,10 +4331,12 @@ struct
pop_imports () ;
Some (Dmodule(name,l,[],None,loc))
- | LDimport(None,id,alias) ->
- add_import ?alias id ; None
+ | LDimport ({import_loader = None; _} as import) ->
+ add_import ?alias:import.module_alias import.module_name ; None
- | LDimport(Some (name, plugin) as loader,id,alias) ->
+ | LDimport ({import_loader = Some loader; _} as import) ->
+ let name, plugin = loader.loader_name, loader.loader_plugin in
+ let id = import.module_name in
let annot =
match Logic_env.Modules.find id with
| None, oldloc ->
@@ -4349,9 +4355,12 @@ struct
let builder = make_module_builder decls id in
let path = Logic_utils.longident id in
Extensions.importer ~plugin name ~builder ~loc path ;
- Logic_env.Modules.add id (loader,loc) ;
- Some (Dmodule(id,List.rev !decls,[],loader,loc))
- in add_import ?alias id ; annot
+ Logic_env.Modules.add id (Some (name, plugin),loc) ;
+ let loader : Cil_types.loader =
+ {loader_name = name; loader_plugin = plugin}
+ in
+ Some (Dmodule(id,List.rev !decls,[],Some loader,loc))
+ in add_import ?alias:import.module_alias id ; annot
| LDtype(name,l,def) ->
let env = init_type_variables loc l in
@@ -4498,16 +4507,21 @@ struct
let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
Some (Dvolatile (tsets, rvi_opt, wvi_opt, [], loc))
- | LDextended (Ext_lexpr(name, plugin, content)) ->
+ | LDextended (Ext_lexpr ext) ->
+ let plugin, name = ext.ext_plugin, ext.ext_name in
let typing_context = base_ctxt (Lenv.empty ()) in
- let status,tcontent = Extensions.typer ~plugin name ~typing_context ~loc content in
+ let status,tcontent =
+ Extensions.typer ~plugin name ~typing_context ~loc ext.ext_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)) ->
+ | LDextended (Ext_extension gext) ->
+ let plugin, name = gext.gext_plugin, gext.gext_name in
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent =
- Extensions.typer_block name ~plugin ~typing_context ~loc (kind,content)
+ Extensions.typer_block name ~plugin ~typing_context ~loc
+ (gext.gext_kind,gext.gext_content)
in
let textended = Logic_const.new_acsl_extension ~plugin name loc status tcontent in
Some (Dextended (textended, [], loc))
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 2315b025d2c09ad278ef14f23770de394d537342..2669ced475387e4835a49716b5079143ea86bcb5 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -168,7 +168,11 @@ type toplevel_predicate =
(** ACSL extension.
@before Frama-C+dev Was of type [string * lexpr list].
*)
-type extension = string * string * lexpr list
+type extension = {
+ ext_name: string;
+ ext_plugin: string;
+ ext_content: lexpr list;
+}
(** type invariant. *)
type type_annot = {inv_name: string;
@@ -189,6 +193,14 @@ type typedef =
(** sum type, list of constructors *)
| TDsyn of logic_type (** synonym of an existing type *)
+type loader = {
+ loader_name: string;
+ loader_plugin: string;
+}
+(** loader type used by module importers.
+ @since Frama-C+dev
+*)
+
(** global declarations. *)
type decl = {
decl_node : decl_node; (** kind of declaration. *)
@@ -250,7 +262,11 @@ and decl_node =
| LDmodule of string * decl list
(** [LDmodule(id,decls)]
represents a module of axiomatic definitions.*)
- | LDimport of (string * string) option * string * string option
+ | LDimport of {
+ import_loader: loader option;
+ module_name: string;
+ module_alias: string option;
+ }
(** [LDimport(loader,module,alias)]
imports symbols from module using the specified loader,
with optional alias.*)
@@ -288,10 +304,15 @@ and variant = lexpr * string option
(** Global ACSL extension. *)
and global_extension =
- | Ext_lexpr of string * string * lexpr list
+ | Ext_lexpr of extension
(** @before Frama-C+dev Was of type [string * lexpr list]. *)
- | Ext_extension of string * string * string * extended_decl list
+ | Ext_extension of {
+ gext_name:string;
+ gext_plugin:string;
+ gext_kind: string;
+ gext_content: extended_decl list;
+ }
(** @before Frama-C+dev Was of type [string * string * extended_decl list]. *)
and extended_decl = {
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index a4a0b4bf026316bca8a406f026c5e96bafffff1c..238da2082829c7c7e24bb9b5492d0f7425b6fd55 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -12,11 +12,17 @@ let ext_typing_fooo _typing_context _loc l =
let ext_typing_block typing_context loc_here node =
match node.extended_node with
- | Ext_lexpr (name,plugin,data) ->
+ | Ext_lexpr ext ->
+ let name, plugin, data = ext.ext_name, ext.ext_plugin, ext.ext_content in
let status,kind = Logic_typing.get_typer ~plugin name ~typing_context ~loc:node.extended_loc data in
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
+ | Ext_extension gext ->
+ let name, plugin = gext.gext_name, gext.gext_plugin in
+ let kind, data = gext.gext_kind, gext.gext_content in
+ let status,kind =
+ Logic_typing.get_typer_block ~plugin name ~typing_context
+ ~loc:node.extended_loc (kind,data)
+ in
Logic_const.new_acsl_extension ~plugin name loc_here status kind
let ext_typing_foo typing_context loc (s,d) =