From 391c64c3b7ac7a09f9ff544ef27f6b3fc0806e4c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 20 Aug 2024 12:35:17 +0200
Subject: [PATCH] [modules] check for duplicate imports
---
src/kernel_services/ast_queries/logic_env.ml | 7 +++-
src/kernel_services/ast_queries/logic_env.mli | 3 +-
.../ast_queries/logic_typing.ml | 32 ++++++++++++-------
3 files changed, 28 insertions(+), 14 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 585945a27d..04d065b5b9 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -156,8 +156,13 @@ module Axiomatics =
let size = 17
end)
+module ModuleOccurence =
+ Datatype.Pair
+ (Datatype.Option(Datatype.String)) (* external driver *)
+ (Cil_datatype.Location)
+
module Modules =
- State_builder.Hashtbl(Datatype.String.Hashtbl)(Cil_datatype.Location)
+ State_builder.Hashtbl(Datatype.String.Hashtbl)(ModuleOccurence)
(struct
let name = "Logic_env.Modules"
let dependencies = []
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index 599b81ae0f..7bdbb547c3 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -66,7 +66,8 @@ module Axiomatics: State_builder.Hashtbl
(** @since Frama-C+dev *)
module Modules: State_builder.Hashtbl
- with type key = string and type data = Cil_types.location
+ with type key = string
+ and type data = string option * Cil_types.location (* driver, loc *)
val builtin_states: State.t list
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 2b115f6ab6..ea02461aaf 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4311,11 +4311,11 @@ struct
end;
let name = fullname ~context id in
let context = InModule name in
- let change oldloc =
+ let change (_,oldloc) =
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);
+ ignore (Logic_env.Modules.memo ~change (fun _ -> (None,loc)) name);
push_imports () ;
add_import ~current:true name ;
let l = List.filter_map (decl ~context) decls in
@@ -4327,16 +4327,24 @@ struct
| LDimport(Some driver as drv,name,alias) ->
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
+ match Logic_env.Modules.find name with
+ | None, oldloc ->
+ C.error loc
+ "Module %s already defined (at %a)"
+ name Cil_printer.pp_location oldloc
+ | Some odrv, oldloc ->
+ if odrv <> driver then
+ C.error loc
+ "Module %s already imported with driver %s (at %a)"
+ name odrv Cil_printer.pp_location oldloc
+ else None
+ | exception Not_found ->
+ 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 (drv,loc) ;
+ Some (Dmodule(name,List.rev !decls,[],drv,loc))
in add_import ?alias name ; annot
| LDtype(name,l,def) ->
--
GitLab