From 5d8b8dc3349fedbf788a88f70feb4feb17aa7b6d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 21 Aug 2024 16:35:26 +0200
Subject: [PATCH] [modules] fixed scope after sub-module closing
---
src/kernel_services/ast_printing/cil_printer.ml | 1 -
src/kernel_services/ast_queries/logic_typing.ml | 10 ++++++++--
tests/spec/oracle/submodule.res.oracle | 17 ++++++++++++++++-
tests/spec/submodule.i | 12 +++++++++++-
4 files changed, 35 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index fa0a5d3969..9adb18b2e8 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2721,7 +2721,6 @@ class cil_printer () = object (self)
method term_lhost fmt (lh:term_lhost) =
self#term_lval fmt (lh, TNoOffset)
-
val module_stack : string Stack.t = Stack.create ()
method logic_name fmt a =
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d2c1933941..29d7037689 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -738,9 +738,15 @@ struct
let pop_imports () =
begin
- let c,s = Stack.pop scopes in
+ let closed = !current_scope in
+ let c,cs = Stack.pop scopes in
+ let cs =
+ match closed with
+ | Some s when c <> None -> s :: cs
+ | _ -> cs
+ in
current_scope := c ;
- imported_scopes := s ;
+ imported_scopes := cs ;
end
let add_import ?(current=false) ?alias name =
diff --git a/tests/spec/oracle/submodule.res.oracle b/tests/spec/oracle/submodule.res.oracle
index b58a753739..4ccdc877c0 100644
--- a/tests/spec/oracle/submodule.res.oracle
+++ b/tests/spec/oracle/submodule.res.oracle
@@ -7,10 +7,25 @@ module Foo {
logic t elt;
module Bar {
- predicate test(Foo::t x) = x ≡ Foo::elt;
+ predicate test1(Foo::t x) = x ≡ Foo::elt;
+
+ predicate test2(Foo::t x, Foo::t y) = test1(x) ∧ test1(y);
+
+ module Jazz {
+ predicate test3(Foo::t x) = Foo::Bar::test2(x, x);
+
+ predicate test4(Foo::t y) = Foo::Bar::test1(y);
+
+ }
}
+ predicate test5(t y) = Bar::test2(y, y);
+
+ predicate test6(t y) = Bar::Jazz::test3(y);
+
+ predicate test7(t z) = Bar::test1(z);
+
}
*/
diff --git a/tests/spec/submodule.i b/tests/spec/submodule.i
index d57036e0c5..1fc8a01411 100644
--- a/tests/spec/submodule.i
+++ b/tests/spec/submodule.i
@@ -3,7 +3,17 @@
type t;
logic t elt;
module Bar {
- predicate test(t x) = x == Foo::elt;
+ predicate test1(t x) = x == Foo::elt;
+ predicate test2(t x, t y) = test1(x) && test1(y);
+
+ module Jazz {
+ predicate test3(t x) = test2(x,x);
+ predicate test4(t y) = Bar::test1(y);
+ }
+
}
+ predicate test5(t y) = Bar::test2(y,y);
+ predicate test6(t y) = Bar::Jazz::test3(y);
+ predicate test7(t z) = Foo::Bar::test1(z);
}
*/
--
GitLab