From a97092012932bc2d16da2c8bc2f65fc401f9e932 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Jul 2024 16:30:33 +0200
Subject: [PATCH] [kernel] fix absolute names in imported modules
---
src/kernel_services/ast_queries/acsl_extension.mli | 2 +-
src/kernel_services/ast_queries/logic_typing.ml | 4 +++-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index d5c76f546f..a8889b0899 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -173,7 +173,7 @@ val register_code_annot_next_both: register_extension
New type and function symbols shall be created with `Cil.make_xxx` functions.
The registered symbols {i will} be automatically prefixed with the name of
- the imported module.
+ the imported module if necessary.
The register module importer function might be invoked several times,
typically when a given module is imported from several files. Although
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f2158c1dc0..22360e6fe5 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -854,7 +854,9 @@ struct
end
let make_module_builder (decls : global_annotation list ref) moduleId =
- let wrap = Printf.sprintf "%s::%s" moduleId in
+ let prefix = moduleId ^ "::" in
+ let wrap s =
+ if String.starts_with ~prefix s then s else prefix ^ s in
let add_logic_ctor loc ct =
ct.ctor_name <- wrap ct.ctor_name ;
add_logic_ctor loc ct in
--
GitLab