From e6ac75eefe5c997a757c14461cb4b39fda5e5102 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:36:13 +0200
Subject: [PATCH] [kernel] reload imported
---
.../ast_queries/logic_typing.ml | 24 ++++++++++++-------
tests/spec/import.i | 6 +++--
tests/spec/oracle/import.0.res.oracle | 6 +++++
tests/spec/oracle/import.1.res.oracle | 6 +++++
4 files changed, 31 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index b700d1f25e..f2158c1dc0 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -758,7 +758,7 @@ struct
let add_import ?(current=false) ?alias name =
begin
- let short = match alias with Some a -> a | None ->
+ let short = match alias with Some "_" -> "" | Some a -> a | None ->
List.hd @@ List.rev @@ Logic_utils.longident name in
let s = {
long_prefix = name ^ "::";
@@ -4303,8 +4303,8 @@ struct
C.error loc
"Duplicated axiomatics %s (first occurrence at %a)"
id Cil_printer.pp_location oldloc in
- let l = List.filter_map (decl ~context:InAxiomatic) decls in
ignore (Logic_env.Axiomatics.memo ~change (fun _ -> loc) id);
+ let l = List.filter_map (decl ~context:InAxiomatic) decls in
Some (Daxiomatic(id,l,[],loc))
| LDmodule(id,decls) ->
@@ -4320,23 +4320,29 @@ struct
C.error loc
"Duplicated module %s (first occurrence at %a)"
id Cil_printer.pp_location oldloc in
+ ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
push_imports () ;
add_import ~current:true name ;
let l = List.filter_map (decl ~context) decls in
pop_imports () ;
- ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
Some (Dmodule(name,l,[],None,loc))
| LDimport(None,name,alias) ->
add_import ?alias name ; None
| 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,[],drv,loc))
+ let annot =
+ if not @@ Logic_env.Modules.mem name then
+ begin
+ 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 ;
+ Logic_env.Modules.add name loc ;
+ Some (Dmodule(name,List.rev !decls,[],drv,loc))
+ end
+ else None
+ in add_import ?alias name ; annot
| LDtype(name,l,def) ->
let env = init_type_variables loc l in
diff --git a/tests/spec/import.i b/tests/spec/import.i
index 82ef19a692..837dffbac7 100644
--- a/tests/spec/import.i
+++ b/tests/spec/import.i
@@ -6,6 +6,8 @@ OPT: -print -kernel-msg-key printer:imported-modules
/*@ import foo: A::B; */
/*@ predicate check1(B::t x) = B::check(x,0); */
+/*@ predicate check2(A::B::t x) = A::B::check(x,0); */
-/* import foo: A::B \as C; */
-/* predicate check2(C::t x) = A::B::check(x,0); */
+/*@ import foo: A::B \as C; */
+/*@ predicate check3(C::t x) = C::check(x,0); */
+/*@ predicate check4(C::t x) = A::B::check(x,0); */
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
index 22a7a7d111..f0f5707e2b 100644
--- a/tests/spec/oracle/import.0.res.oracle
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -7,4 +7,10 @@
*/
/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
*/
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
diff --git a/tests/spec/oracle/import.1.res.oracle b/tests/spec/oracle/import.1.res.oracle
index 3a070d6021..b5236c1c99 100644
--- a/tests/spec/oracle/import.1.res.oracle
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -13,4 +13,10 @@
*/
/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
*/
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
--
GitLab