From 55b4eb1c46c1179003a30feb19268eb716e00a9d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 20 Jun 2024 08:36:52 +0200
Subject: [PATCH] [kernel] fix mergeCil with modules
---
src/kernel_internals/typing/mergecil.ml | 2 +-
src/kernel_services/ast_queries/logic_env.ml | 2 ++
tests/spec/bar.i | 10 ++++++++++
tests/spec/foo.i | 11 +++++++++++
tests/spec/oracle/foo.res.oracle | 11 +++++++++++
5 files changed, 35 insertions(+), 1 deletion(-)
create mode 100644 tests/spec/bar.i
create mode 100644 tests/spec/foo.i
create mode 100644 tests/spec/oracle/foo.res.oracle
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index b4d19c325b..4ce813edc8 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -643,7 +643,7 @@ let lfEq = LogicMerging.create_eq_table 111 (* Logic functions *)
let ltEq = PlainMerging.create_eq_table 111 (* Logic types *)
let lcEq = PlainMerging.create_eq_table 111 (* Logic constructors *)
-let laEq = PlainMerging.create_eq_table 111 (* Axiomatics *)
+let laEq = PlainMerging.create_eq_table 111 (* Axiomatics & Modules *)
let llEq = PlainMerging.create_eq_table 111 (* Lemmas *)
let lvEq = VolatileMerging.create_eq_table 111
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 09a6dbce04..585945a27d 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -183,6 +183,7 @@ let init_dependencies from =
Logic_ctor_info.self;
Lemmas.self;
Axiomatics.self;
+ Modules.self;
Model_info.self;
]
@@ -350,6 +351,7 @@ let prepare_tables () =
Logic_info.clear ();
Lemmas.clear ();
Axiomatics.clear();
+ Modules.clear();
Model_info.clear ();
Logic_type_builtin.iter Logic_type_info.add;
Logic_ctor_builtin.iter Logic_ctor_info.add;
diff --git a/tests/spec/bar.i b/tests/spec/bar.i
new file mode 100644
index 0000000000..8ebaf7de02
--- /dev/null
+++ b/tests/spec/bar.i
@@ -0,0 +1,10 @@
+/* run.config
+ DONTRUN: Companion file of foo.i
+*/
+
+/*@
+ module A {
+ type t;
+ logic t op(t x);
+ }
+ */
diff --git a/tests/spec/foo.i b/tests/spec/foo.i
new file mode 100644
index 0000000000..f41b48bf59
--- /dev/null
+++ b/tests/spec/foo.i
@@ -0,0 +1,11 @@
+/* run.config
+ DEPS: bar.i
+ OPT: bar.i -print
+ */
+
+/*@
+ module A {
+ type t;
+ logic t op(t x);
+ }
+ */
diff --git a/tests/spec/oracle/foo.res.oracle b/tests/spec/oracle/foo.res.oracle
new file mode 100644
index 0000000000..50873ff7f5
--- /dev/null
+++ b/tests/spec/oracle/foo.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing foo.i (no preprocessing)
+[kernel] Parsing bar.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ module A {
+ type t;
+
+ logic t op(t x) ;
+
+ }
+ */
+
--
GitLab