From 56c0a39b64a67e18a2a11368cb48d3fe3e6aa7a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 18 Sep 2024 17:29:52 +0200
Subject: [PATCH] [acsl] fix current scopes
---
.../ast_queries/logic_typing.ml | 26 ++++++++++++-------
src/plugins/wp/tests/wp_plugin/module.i | 4 +--
tests/spec/module.i | 4 +--
3 files changed, 20 insertions(+), 14 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 99209cf64b3..541a190501d 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -715,6 +715,7 @@ struct
(* Imported Scope *)
type scope = {
+ current: bool; (* accepted for non-qualified names *)
long_prefix: string; (* last '::' included *)
short_prefix: string; (* last '::' included *)
}
@@ -724,15 +725,18 @@ struct
let current_scope : scope option ref = ref None
let imported_scopes : scope list ref = ref []
- let current_scopes () =
+ let all_scopes () =
match !current_scope with
| None -> !imported_scopes
| Some s -> s :: !imported_scopes
+ let current_scopes () =
+ List.filter (fun s -> s.current) @@ all_scopes ()
+
let push_imports () =
let current = !current_scope in
let imported = !imported_scopes in
- let all = current_scopes () in
+ let all = all_scopes () in
Stack.push (current,imported) scopes ;
imported_scopes := all
@@ -759,6 +763,7 @@ struct
List.hd @@ List.rev @@ Logic_utils.longident name
in
let s = {
+ current;
long_prefix = name ^ "::";
short_prefix = short ^ "::";
} in
@@ -771,14 +776,15 @@ struct
let find_import fn a =
let find_opt b = try Some (fn b) with Not_found -> None in
if Logic_utils.is_qualified a then
- let in_scope s = String.starts_with ~prefix:s.short_prefix a in
- find_opt @@
- match List.find_opt in_scope @@ current_scopes () with
- | None -> a
- | Some s ->
- let p = String.length s.short_prefix in
- let n = String.length a in
- s.long_prefix ^ String.sub a p (n-p)
+ let resolved_name =
+ let has_short_prefix s = String.starts_with ~prefix:s.short_prefix a in
+ match List.find_opt has_short_prefix @@ all_scopes () with
+ | None -> a
+ | Some s ->
+ let p = String.length s.short_prefix in
+ let n = String.length a in
+ s.long_prefix ^ String.sub a p (n-p)
+ in find_opt resolved_name
else
let find_in_scope s = find_opt (s.long_prefix ^ a) in
match List.find_map find_in_scope @@ current_scopes () with
diff --git a/src/plugins/wp/tests/wp_plugin/module.i b/src/plugins/wp/tests/wp_plugin/module.i
index a237203c4fa..9a65901b4a0 100644
--- a/src/plugins/wp/tests/wp_plugin/module.i
+++ b/src/plugins/wp/tests/wp_plugin/module.i
@@ -7,8 +7,8 @@
}
module foo::Jazz {
import foo::Bar \as X;
- logic t inv(X::t x);
- logic t opN(t x, integer n) = n >= 0 ? X::opN(x,n) : X::opN(inv(x),-n);
+ logic X::t inv(X::t x);
+ logic X::t opN(X::t x, integer n) = n >= 0 ? X::opN(x,n) : X::opN(inv(x),-n);
}
import foo::Bar \as A;
import foo::Jazz \as B;
diff --git a/tests/spec/module.i b/tests/spec/module.i
index 80f34a59aa8..3dbcb977243 100644
--- a/tests/spec/module.i
+++ b/tests/spec/module.i
@@ -11,8 +11,8 @@
}
module foo::bar {
import Foo \as X;
- logic t inv(X::t x);
- logic t opN(t x, integer n) = n >= 0 ? X::opN(x,n) : opN(inv(x),-n);
+ logic X::t inv(X::t x);
+ logic X::t opN(X::t x, integer n) = n >= 0 ? X::opN(x,n) : opN(inv(x),-n);
}
import Foo \as A;
import foo::bar \as B;
--
GitLab