From 9bc3cf26f1cc6eb4eee34be699d437a175c56eac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 21 Jun 2024 11:19:12 +0200
Subject: [PATCH] [kernel] print imported module
---
src/kernel_internals/typing/mergecil.ml | 178 +++++++++---------
src/kernel_services/ast_data/annotations.ml | 4 +-
src/kernel_services/ast_data/cil_types.ml | 3 +-
src/kernel_services/ast_data/property.ml | 2 +-
.../ast_printing/cil_printer.ml | 12 +-
.../ast_printing/cil_types_debug.ml | 6 +-
src/kernel_services/ast_queries/ast_diff.ml | 2 +-
src/kernel_services/ast_queries/cil.ml | 8 +-
.../ast_queries/cil_datatype.ml | 18 +-
src/kernel_services/ast_queries/file.ml | 2 +-
.../ast_queries/logic_typing.ml | 6 +-
.../ast_queries/logic_utils.ml | 8 +-
.../plugin_entry_points/kernel.ml | 2 +
.../plugin_entry_points/kernel.mli | 2 +
src/plugins/gui/filetree.ml | 2 +-
src/plugins/metrics/metrics_cilast.ml | 2 +-
src/plugins/metrics/metrics_pivot.ml | 2 +-
src/plugins/wp/LogicUsage.ml | 2 +-
tests/spec/import.i | 1 +
tests/spec/oracle/import.0.res.oracle | 10 +
...{import.res.oracle => import.1.res.oracle} | 5 +-
21 files changed, 154 insertions(+), 123 deletions(-)
create mode 100644 tests/spec/oracle/import.0.res.oracle
rename tests/spec/oracle/{import.res.oracle => import.1.res.oracle} (79%)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 4ce813edc82..cbbebbd4f3c 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -858,9 +858,9 @@ let rec global_annot_without_irrelevant_attributes ga =
| Daxiomatic(n,l,attr,loc) ->
Daxiomatic(n,List.map global_annot_without_irrelevant_attributes l,
drop_attributes_for_merge attr,loc)
- | Dmodule(n,l,attr,loc) ->
+ | Dmodule(n,l,attr,drv,loc) ->
Dmodule(n,List.map global_annot_without_irrelevant_attributes l,
- drop_attributes_for_merge attr,loc)
+ drop_attributes_for_merge attr,drv,loc)
| Dlemma (id,labs,typs,st,attr,loc) ->
Dlemma (id,labs,typs,st,drop_attributes_for_merge attr,loc)
| Dtype (lti,loc) ->
@@ -896,12 +896,11 @@ let rec global_annot_pass1 g =
if Option.is_some wvi then process_term_kind (x,W))
hs
| Daxiomatic(id,decls,_,l) ->
- ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls)
+ ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls,None)
(Some (l,!currentDeclIdx)));
List.iter global_annot_pass1 decls
- | Dmodule(id,decls,_,l) ->
- Current_loc.set l;
- ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls)
+ | Dmodule(id,decls,_,drv,l) ->
+ ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls,drv)
(Some (l,!currentDeclIdx)));
List.iter global_annot_pass1 decls
| Dfun_or_pred (li,l) ->
@@ -1444,17 +1443,17 @@ let matchLogicCtor oldfidx oldpi fidx pi =
"invalid multiple logic constructors declarations %s" pi.ctor_name
(* ignores irrelevant attributes such as __fc_stdlib *)
-let matchLogicAxiomatic oldfidx (oldid,_ as oldnode) fidx (id,_ as node) =
+let matchLogicAxiomatic oldfidx (oldid,_,_ as oldnode) fidx (id,_,_ as node) =
let oldanode = PlainMerging.getNode laEq laSyn oldfidx oldid oldnode None in
let anode = PlainMerging.getNode laEq laSyn fidx id node None in
if oldanode != anode then begin
- let _, oldax = oldanode.ndata in
+ let _, oldax, odrv = oldanode.ndata in
let oldaidx = oldanode.nfidx in
- let _, ax = anode.ndata in
+ let _, ax, drv = anode.ndata in
let aidx = anode.nfidx in
let ax = List.map global_annot_without_irrelevant_attributes ax in
let oldax = List.map global_annot_without_irrelevant_attributes oldax in
- if Logic_utils.is_same_axiomatic oldax ax then begin
+ if Logic_utils.is_same_axiomatic oldax ax && odrv = drv then begin
if oldaidx < aidx then
anode.nrep <- oldanode.nrep
else
@@ -1720,79 +1719,79 @@ let oneFilePass1 (f:file) : unit =
let iter g =
let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
- | GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
- incr currentDeclIdx;
- if vi.vstorage <> Static then begin
- matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
- end
-
- | GFun (fdec, l) ->
- incr currentDeclIdx;
- (* Save the names of the formal arguments *)
- let _, args, _, _ = splitFunctionTypeVI fdec.svar in
- H.add formalNames (!currentFidx, fdec.svar.vname)
- (List.map (fun (n,_,_) -> n) (argsToList args));
- (* Force inline functions to be static. *)
- (* GN: This turns out to be wrong. inline functions are external,
- * unless specified to be static. *)
- (*
- if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
- fdec.svar.vstorage <- Static;
- *)
- if fdec.svar.vstorage <> Static then begin
- matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
- end else begin
- if fdec.svar.vinline && mergeInlines then
- (* Just create the nodes for inline functions *)
- ignore (PlainMerging.getNode iEq iSyn !currentFidx
- fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
- end
- (* Make nodes for the defined type and structure tags *)
- | GType (t, l) ->
- incr currentDeclIdx;
- t.treferenced <- false;
- if t.tname <> "" then (* The empty names are just for introducing
- * undefined comp tags *)
- ignore (PlainMerging.getNode tEq tSyn !currentFidx t.tname t
- (Some (l, !currentDeclIdx)))
- else begin (* Go inside and clean the referenced flag for the
- * declared tags *)
- match t.ttype with
- TComp (ci, _ ) ->
- ci.creferenced <- false;
- (* Create a node for it *)
- ignore
- (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci None)
-
- | TEnum (ei, _) ->
- ei.ereferenced <- false;
- ignore
- (EnumMerging.getNode eEq eSyn !currentFidx ei ei None)
-
- | _ -> (Kernel.fatal "Anonymous Gtype is not TComp")
- end
+ | GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
+ incr currentDeclIdx;
+ if vi.vstorage <> Static then begin
+ matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
+ end
- | GCompTag (ci, l) ->
- incr currentDeclIdx;
- ci.creferenced <- false;
- ignore (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci
+ | GFun (fdec, l) ->
+ incr currentDeclIdx;
+ (* Save the names of the formal arguments *)
+ let _, args, _, _ = splitFunctionTypeVI fdec.svar in
+ H.add formalNames (!currentFidx, fdec.svar.vname)
+ (List.map (fun (n,_,_) -> n) (argsToList args));
+ (* Force inline functions to be static. *)
+ (* GN: This turns out to be wrong. inline functions are external,
+ * unless specified to be static. *)
+ (*
+ if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
+ fdec.svar.vstorage <- Static;
+ *)
+ if fdec.svar.vstorage <> Static then begin
+ matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
+ end else begin
+ if fdec.svar.vinline && mergeInlines then
+ (* Just create the nodes for inline functions *)
+ ignore (PlainMerging.getNode iEq iSyn !currentFidx
+ fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
+ end
+ (* Make nodes for the defined type and structure tags *)
+ | GType (t, l) ->
+ incr currentDeclIdx;
+ t.treferenced <- false;
+ if t.tname <> "" then (* The empty names are just for introducing
+ * undefined comp tags *)
+ ignore (PlainMerging.getNode tEq tSyn !currentFidx t.tname t
(Some (l, !currentDeclIdx)))
- | GCompTagDecl (ci,_) -> ci.creferenced <- false
- | GEnumTagDecl (ei,_) -> ei.ereferenced <- false
- | GEnumTag (ei, l) ->
- incr currentDeclIdx;
- let orig_name =
- if ei.eorig_name = "" then ei.ename else ei.eorig_name
- in
- ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
- ~lookupname:orig_name ~data:l);
- ei.ereferenced <- false;
- ignore
- (EnumMerging.getNode eEq eSyn !currentFidx ei ei
- (Some (l, !currentDeclIdx)))
+ else begin (* Go inside and clean the referenced flag for the
+ * declared tags *)
+ match t.ttype with
+ TComp (ci, _ ) ->
+ ci.creferenced <- false;
+ (* Create a node for it *)
+ ignore
+ (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci None)
+
+ | TEnum (ei, _) ->
+ ei.ereferenced <- false;
+ ignore
+ (EnumMerging.getNode eEq eSyn !currentFidx ei ei None)
+
+ | _ -> (Kernel.fatal "Anonymous Gtype is not TComp")
+ end
+
+ | GCompTag (ci, l) ->
+ incr currentDeclIdx;
+ ci.creferenced <- false;
+ ignore (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci
+ (Some (l, !currentDeclIdx)))
+ | GCompTagDecl (ci,_) -> ci.creferenced <- false
+ | GEnumTagDecl (ei,_) -> ei.ereferenced <- false
+ | GEnumTag (ei, l) ->
+ incr currentDeclIdx;
+ let orig_name =
+ if ei.eorig_name = "" then ei.ename else ei.eorig_name
+ in
+ ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
+ ~lookupname:orig_name ~data:l);
+ ei.ereferenced <- false;
+ ignore
+ (EnumMerging.getNode eEq eSyn !currentFidx ei ei
+ (Some (l, !currentDeclIdx)))
| GAnnot (gannot, _) ->
- incr currentDeclIdx;
- global_annot_pass1 gannot
+ incr currentDeclIdx;
+ global_annot_pass1 gannot
| GText _ | GPragma _ | GAsm _ -> ()
in
List.iter iter f.globals
@@ -2217,7 +2216,7 @@ let rec logic_annot_pass2 context g a =
Logic_utils.add_logic_function li;
| Some _ -> ()
(* FIXME: should we perform same actions
- as the case Dlogic_reads above ? *)
+ as the case Dlogic_reads above ? *)
end
| Dtype (t, _) ->
begin
@@ -2259,7 +2258,7 @@ let rec logic_annot_pass2 context g a =
(LogicMerging.find_eq_table lfEq (!currentFidx,n)).ndata
| Some _ -> ()
end
- | Dmodel_annot (mf,l) ->
+ | Dmodel_annot (mf, l) ->
begin
match
ModelMerging.findReplacement
@@ -2273,8 +2272,8 @@ let rec logic_annot_pass2 context g a =
mfEq (!currentFidx,(mf'.mi_name,mf'.mi_base_type))
in
(* Adds a new representative. Do not replace directly
- my_node, as there might be some pointers to it from
- other files.
+ my_node, as there might be some pointers to it from
+ other files.
*)
let my_node' = { my_node with ndata = mf' } in
my_node.nrep <- my_node'; (* my_node' represents my_node *)
@@ -2301,7 +2300,7 @@ let rec logic_annot_pass2 context g a =
mergePushGlobals (visitCilGlobal renameVisitor g)
| Some _ -> ()
end
- | Dvolatile(vi,rd,wr,attr,loc) ->
+ | Dvolatile(vi, rd, wr, attr, loc) ->
let is_representative id =
Option.is_none
(VolatileMerging.findReplacement true lvEq !currentFidx id)
@@ -2359,7 +2358,7 @@ let rec logic_annot_pass2 context g a =
| Toplevel -> ()
| InAxiomatic ->
Kernel.abort ~current:true
- "nested axiomatics are not allowed in ACSL";
+ "nested axiomatics are not allowed in ACSL";
| InModule ->
Kernel.abort ~current:true
"mixed axiomatics and modules are not allowed in ACSL";
@@ -2368,9 +2367,8 @@ let rec logic_annot_pass2 context g a =
List.iter (logic_annot_pass2 InAxiomatic g) l
| Some _ -> ()
end
- | Dmodule(n,l,_,loc) ->
+ | Dmodule(n, l, _, _, _) ->
begin
- Current_loc.set loc;
match PlainMerging.findReplacement true laEq !currentFidx n with
None ->
begin match context with
@@ -3004,8 +3002,8 @@ let oneFilePass2 (f: file) =
end
| GCompTagDecl (ci, _) -> begin
(* This is here just to introduce an undefined
- * structure. But maybe the structure was defined
- * already. *)
+ * structure. But maybe the structure was defined
+ * already. *)
(* Do not increment currentDeclIdx because it is not incremented in
* pass 1*)
if H.mem emittedCompDecls ci.cname then
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index c2f26d3a55a..94d46e207b8 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1690,7 +1690,7 @@ let rec remove_declared_global_annot logic_vars = function
| Dvolatile _ | Dtype _ | Dlemma _ | Dmodel_annot _
| Dextended _ ->
logic_vars
- | Daxiomatic (_,l,_, _) | Dmodule (_,l,_, _) ->
+ | Daxiomatic (_,l,_,_) | Dmodule (_,l,_,_,_) ->
List.fold_left remove_declared_global_annot logic_vars l
let remove_declared_global c_vars logic_vars = function
@@ -1806,7 +1806,7 @@ let logic_info_of_global s =
let rec check_one acc = function
| Dfun_or_pred(li,_) | Dinvariant(li,_) | Dtype_annot(li,_) ->
check_logic_info li acc
- | Daxiomatic (_,l, _, _) | Dmodule (_,l, _, _) ->
+ | Daxiomatic (_,l, _, _) | Dmodule (_,l, _, _, _) ->
List.fold_left check_one acc l
| Dtype _ | Dvolatile _ | Dlemma _ | Dmodel_annot _
| Dextended _
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index ff8cade0ca3..b29782e0d6c 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1800,7 +1800,8 @@ and global_annotation =
* attributes * location
(** associated terms, reading function, writing function *)
| Daxiomatic of string * global_annotation list * attributes * location
- | Dmodule of string * global_annotation list * attributes * location
+ (** last string option is the external importer responsible for the module *)
+ | Dmodule of string * global_annotation list * attributes * 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_data/property.ml b/src/kernel_services/ast_data/property.ml
index b1460dbef17..d609dca1c2b 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1520,7 +1520,7 @@ let ip_of_global_annotation a =
| Daxiomatic(iax_name, l, iax_attrs, _) ->
let iax_props = List.fold_left aux [] l in
IPAxiomatic {iax_name; iax_props; iax_attrs} :: (iax_props @ acc)
- | Dmodule(im_name, l, im_attrs, _) ->
+ | Dmodule(im_name, l, im_attrs, _, _) ->
let im_props = List.fold_left aux [] l in
IPModule {im_name; im_props; im_attrs} :: (im_props @ acc)
| Dlemma(il_name, il_labels, il_args, il_pred, il_attrs, il_loc) ->
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index fc2a377fd53..4f208682046 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3423,10 +3423,18 @@ class cil_printer () = object (self)
(Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
self#global_annotation)
decls
- | Dmodule(id,decls,_attr, _) ->
+ | Dmodule(id, _, _, Some drv, _)
+ when not Kernel.(is_debug_key_enabled dkey_print_imported_modules) ->
+ fprintf fmt "@[<hov 2>%a %s: %s %a _ ;@]@\n"
+ self#pp_acsl_keyword "import" drv id
+ self#pp_acsl_keyword "\\as"
+ | Dmodule(id, decls, _attr, driver, _) ->
begin
(* attributes are meant to be purely internal for now. *)
- fprintf fmt "@[<v 2>@[%a %a {@]"
+ fprintf fmt "@[<v 2>@[" ;
+ if Kernel.(is_debug_key_enabled dkey_print_imported_modules) then
+ Option.iter (fprintf fmt "// import %s:@\n") driver ;
+ fprintf fmt "%a %a {@]"
self#pp_acsl_keyword "module" self#logic_name id ;
try
Stack.push (id ^ "::") module_stack ;
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 745b403090a..28e5f944892 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -971,10 +971,10 @@ and pp_global_annotation fmt = function
Format.fprintf fmt "Daxiomatic(%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
pp_attributes attributes pp_location location
- | Dmodule(string,global_annotation_list,attributes,location) ->
- Format.fprintf fmt "Dmodule(%a,%a,%a,%a)" pp_string string
+ | Dmodule(string,global_annotation_list,attributes,driver,location) ->
+ Format.fprintf fmt "Dmodule(%a,%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
- pp_attributes attributes pp_location location
+ pp_attributes attributes (pp_option pp_string) driver pp_location location
| Dtype(logic_type_info,location) ->
Format.fprintf fmt "Dtype(%a,%a)" pp_logic_type_info logic_type_info pp_location location
| Dlemma(string,logic_label_list,string_list,predicate,attributes,location) ->
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 749a1f3d111..7fe9adc6eca 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1517,7 +1517,7 @@ let rec gannot_correspondence =
| Dvolatile _ -> ()
(* reading and writing function themselves will be checked elsewhere. *)
- | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_) ->
+ | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_,_) ->
List.iter gannot_correspondence l
| Dtype (ti,loc) -> ignore (logic_type_correspondence ~loc ti empty_env)
| Dlemma _ -> ()
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index dc3aa585729..4aca4612649 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1919,10 +1919,10 @@ and childrenAnnotation vis a =
let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
let attr' = visitCilAttributes vis attr in
if l' != l || attr != attr' then Daxiomatic(id,l',attr',loc) else a
- | Dmodule(id,l,attr,loc) ->
+ | Dmodule(id,l,attr,drv,loc) ->
let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
let attr' = visitCilAttributes vis attr in
- if l' != l || attr != attr' then Dmodule(id,l',attr',loc) else a
+ if l' != l || attr != attr' then Dmodule(id,l',attr',drv,loc) else a
| Dextended (e,attr,loc) ->
let e' = visitCilExtended vis e in
let attr' = visitCilAttributes vis attr in
@@ -2178,7 +2178,7 @@ and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
let last = mkStmt ~ghost:res.ghost res.skind in
let block = mkBlockNonScoping (List.map make instr_list @ [ last ]) in
block.battrs <- addAttribute (Attr (vis_tmp_attr, [])) block.battrs;
- (* Make our statement contain the instructions to prepend *)
+ (* Make our statement contain the instructions to prepend *)
res.skind <- Block block;
vis#pop_stmt s; res
@@ -5255,7 +5255,7 @@ let mapGlobals (fl: file)
let global_annotation_attributes = function
| Dfun_or_pred ({l_var_info = { lv_attr }}, _) -> lv_attr
| Dvolatile (_,_,_,attrs,_) -> attrs
- | Daxiomatic (_,_,attrs,_) | Dmodule(_,_,attrs,_) -> attrs
+ | Daxiomatic (_,_,attrs,_) | Dmodule(_,_,attrs,_,_) -> attrs
| Dtype ({ lt_attr }, _) -> lt_attr
| Dlemma (_,_,_,_,attrs,_) -> attrs
| Dinvariant ({l_var_info = { lv_attr }}, _) -> lv_attr
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index bd87f8264e0..7f6d2ff8823 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2219,8 +2219,16 @@ module Global_annotation = struct
if res = 0 then Attributes.compare attr1 attr2 else res
| Daxiomatic _, _ -> -1
| _, Daxiomatic _ -> 1
- | Dmodule (m1,_,_,_), Dmodule (m2,_,_,_) ->
- String.compare m1 m2
+ | Dmodule (m1,g1,attr1,drv1,_), Dmodule (m2,g2,attr2,drv2,_) ->
+ let res = String.compare m1 m2 in
+ if res = 0 then
+ let res = compare_list compare g1 g2 in
+ if res = 0 then
+ let res = Stdlib.compare drv1 drv2 in
+ if res = 0 then Attributes.compare attr1 attr2
+ else res
+ else res
+ else res
| Dmodule _, _ -> -1
| _, Dmodule _ -> 1
| Dtype(t1,_), Dtype(t2,_) -> Logic_type_info.compare t1 t2
@@ -2254,7 +2262,7 @@ module Global_annotation = struct
| Daxiomatic (_,[],_,_) -> 5
(* Empty axiomatic is weird but authorized. *)
| Daxiomatic (_,g::_,_,_) -> 5 * hash g
- | Dmodule (m,_,_,_) -> 5 * Datatype.String.hash m
+ | Dmodule (m,_,_,_,_) -> 5 * Datatype.String.hash m
| Dtype (t,_) -> 7 * Logic_type_info.hash t
| Dlemma(n,_,_,_,_,_) -> 11 * Datatype.String.hash n
| Dinvariant(l,_) -> 13 * Logic_info.hash l
@@ -2268,7 +2276,7 @@ module Global_annotation = struct
let loc = function
| Dfun_or_pred(_, loc)
| Daxiomatic(_, _, _, loc)
- | Dmodule(_, _, _, loc)
+ | Dmodule(_, _, _, _, loc)
| Dtype (_, loc)
| Dlemma(_, _, _, _, _, loc)
| Dinvariant(_, loc)
@@ -2279,7 +2287,7 @@ module Global_annotation = struct
let attr = function
| Dfun_or_pred({ l_var_info = { lv_attr }}, _) -> lv_attr
- | Daxiomatic(_, _, attr, _) | Dmodule(_, _, attr, _) -> attr
+ | Daxiomatic(_, _, attr, _) | Dmodule(_, _, attr, _, _) -> attr
| Dtype ({lt_attr}, _) -> lt_attr
| Dlemma(_, _, _, _, attr, _) -> attr
| Dinvariant({ l_var_info = { lv_attr }}, _) -> lv_attr
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index d9b52fed187..4c20f878df8 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1255,7 +1255,7 @@ let extract_logic_infos g =
| Dfun_or_pred (li,_) | Dinvariant (li,_) | Dtype_annot (li,_) -> li :: acc
| Dvolatile _ | Dtype _ | Dlemma _
| Dmodel_annot _ | Dextended _ -> acc
- | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_) -> List.fold_left aux acc l
+ | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_,_) -> List.fold_left aux acc l
in aux [] g
let find_logic_info_decl li =
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 376d0465801..b700d1f25ef 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4325,18 +4325,18 @@ struct
let l = List.filter_map (decl ~context) decls in
pop_imports () ;
ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
- Some (Dmodule(name,l,[],loc))
+ Some (Dmodule(name,l,[],None,loc))
| LDimport(None,name,alias) ->
add_import ?alias name ; None
- | LDimport(Some driver,name,alias) ->
+ | LDimport(Some driver as drv,name,alias) ->
let decls = ref [] in
let builder = make_module_builder decls name in
let path = Logic_utils.longident name in
Extensions.importer driver ~builder ~loc path ;
add_import ?alias name ;
- Some (Dmodule(name,List.rev !decls,[],loc))
+ Some (Dmodule(name,List.rev !decls,[],drv,loc))
| LDtype(name,l,def) ->
let env = init_type_variables loc l in
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 0ec2e482eab..8dc2bbe288a 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -739,9 +739,9 @@ let rec add_attribute_glob_annot a g =
| Daxiomatic(n,l,al,loc) ->
Daxiomatic(n,List.map (add_attribute_glob_annot a) l,
Cil.addAttribute a al,loc)
- | Dmodule(n,l,al,loc) ->
+ | Dmodule(n,l,al,drv,loc) ->
Dmodule(n,List.map (add_attribute_glob_annot a) l,
- Cil.addAttribute a al,loc)
+ Cil.addAttribute a al,drv,loc)
| Dtype(ti,_) -> ti.lt_attr <- Cil.addAttribute a ti.lt_attr; g
| Dlemma(n,labs,t,p,al,l) ->
Dlemma(n,labs,t,p,Cil.addAttribute a al,l)
@@ -1230,8 +1230,8 @@ let rec is_same_global_annotation ga1 ga2 =
| Daxiomatic (id1,ga1,attr1,_), Daxiomatic (id2,ga2,attr2,_) ->
id1 = id2 && is_same_list is_same_global_annotation ga1 ga2
&& is_same_attributes attr1 attr2
- | Dmodule (id1,ga1,attr1,_), Dmodule (id2,ga2,attr2,_) ->
- id1 = id2 && is_same_list is_same_global_annotation ga1 ga2
+ | Dmodule (id1,ga1,attr1,drv1,_), Dmodule (id2,ga2,attr2,drv2,_) ->
+ id1 = id2 && is_same_list is_same_global_annotation ga1 ga2 && drv1 = drv2
&& is_same_attributes attr1 attr2
| Dtype (t1,_), Dtype (t2,_) -> is_same_logic_type_info t1 t2
| Dlemma(n1,labs1,typs1,st1,attr1,_),
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 792ea611542..4862cda2cc5 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -104,6 +104,8 @@ let dkey_print_logic_coercions = register_category "printer:logic-coercions"
let dkey_print_logic_types = register_category "printer:logic-types"
+let dkey_print_imported_modules = register_category "printer:imported-modules"
+
let dkey_print_attrs = register_category "printer:attrs"
let dkey_print_sid = register_category "printer:sid"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 33076ff8e30..7db6111f134 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -102,6 +102,8 @@ val dkey_print_logic_coercions: category
val dkey_print_logic_types: category
+val dkey_print_imported_modules: category
+
val dkey_print_sid: category
val dkey_print_unspecified: category
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 6fbec82d38d..140723ca344 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -316,7 +316,7 @@ module MYTREE = struct
Some (global_name li.l_var_info.lv_name)
| Dvolatile _ -> Some "volatile clause"
| Daxiomatic (s, _, _,_) -> Some (global_name s)
- | Dmodule (s, _, _,_) -> Some (global_name s)
+ | Dmodule (s, _, _, _, _) -> Some (global_name s)
| Dtype (lti, _) -> Some (global_name lti.lt_name)
| Dlemma (s, _, _, _, _,_) -> Some (global_name s)
| Dinvariant (li, _) -> Some (global_name li.l_var_info.lv_name)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 82c8d0eb87d..17f41a67080 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -320,7 +320,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
match an with
| Dfun_or_pred (li, _) -> li.l_var_info.lv_name
| Dvolatile (_, _, _, _, _) -> " (Volatile) "
- | Daxiomatic (s, _, _, _) | Dmodule (s, _, _, _) -> s
+ | Daxiomatic (s, _, _, _) | Dmodule (s, _, _, _, _) -> s
| Dtype (lti, _) -> lti.lt_name
| Dlemma (ln, _, _, _, _, _) -> ln
| Dinvariant (toto, _) -> toto.l_var_info.lv_name
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 9cf5c9ac08f..0232ba1dc92 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -143,7 +143,7 @@ let name_of_global_annotation = function
| Dinvariant (li, _)
| Dtype_annot (li, _) -> Some (name_of_logic_info li)
| Daxiomatic (name, _, _, _)
- | Dmodule (name, _, _, _)
+ | Dmodule (name, _, _, _, _)
| Dtype ({lt_name = name}, _)
| Dlemma (name, _, _, _, _, _)
| Dmodel_annot ({mi_name = name}, _)
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index d454697e775..fdac903ee60 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -223,7 +223,7 @@ let ip_of_axiomatic g =
| Some ip -> ip
let axiomatic_of_global ~context = function
- | (Daxiomatic(name,globals,_,loc) | Dmodule(name,globals,_,loc)) as g ->
+ | (Daxiomatic(name,globals,_,loc) | Dmodule(name,globals,_,_,loc)) as g ->
let a = {
ax_name = name ;
ax_position = fst loc ;
diff --git a/tests/spec/import.i b/tests/spec/import.i
index c1ade89958d..82ef19a6927 100644
--- a/tests/spec/import.i
+++ b/tests/spec/import.i
@@ -1,6 +1,7 @@
/* run.config
MODULE: @PTEST_NAME@
OPT: -print
+OPT: -print -kernel-msg-key printer:imported-modules
*/
/*@ import foo: A::B; */
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
new file mode 100644
index 00000000000..22a7a7d111a
--- /dev/null
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -0,0 +1,10 @@
+[test-import] Linking.
+[test-import] Registering 'foo'.
+[kernel] Parsing import.i (no preprocessing)
+[test-import:7] Loading A::B.
+/* Generated by Frama-C */
+/*@ import foo: A::B \as _ ;
+ */
+/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+ */
+
diff --git a/tests/spec/oracle/import.res.oracle b/tests/spec/oracle/import.1.res.oracle
similarity index 79%
rename from tests/spec/oracle/import.res.oracle
rename to tests/spec/oracle/import.1.res.oracle
index 617e7f8cf03..3a070d60217 100644
--- a/tests/spec/oracle/import.res.oracle
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -1,9 +1,10 @@
[test-import] Linking.
[test-import] Registering 'foo'.
[kernel] Parsing import.i (no preprocessing)
-[test-import:6] Loading A::B.
+[test-import:7] Loading A::B.
/* Generated by Frama-C */
-/*@ module A::B {
+/*@ // import foo:
+ module A::B {
type t;
predicate check(t x, ℤ k) ;
--
GitLab