diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml index b4d19c325b8498dbb4febd49c0c82c02073b4fd8..4ce813edc8205426bc6e21e5de3b1203c569fee0 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 09a6dbce04318697b586caaefeae38b307c01750..585945a27dfc77787927f64f34142597c23a83e4 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 0000000000000000000000000000000000000000..8ebaf7de02eccd2f6a4cebff30215e1574d8700a --- /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 0000000000000000000000000000000000000000..f41b48bf59caa03ae48818bbc7b5798d5b0bcd64 --- /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 0000000000000000000000000000000000000000..50873ff7f5d0ac82c0ceba417b17ee722bb6accb --- /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) ; + + } + */ +