From fc529502777f2fbe491daed62d406867f26b63bd Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Wed, 18 Sep 2024 17:54:44 +0200
Subject: [PATCH] [tests] add some negative tests regarding scope resolution

---
 tests/spec/{module.i => module.c}             | 32 +++++++++++++
 ...{module.res.oracle => module.0.res.oracle} |  2 +-
 tests/spec/oracle/module.1.res.oracle         | 46 +++++++++++++++++++
 3 files changed, 79 insertions(+), 1 deletion(-)
 rename tests/spec/{module.i => module.c} (51%)
 rename tests/spec/oracle/{module.res.oracle => module.0.res.oracle} (89%)
 create mode 100644 tests/spec/oracle/module.1.res.oracle

diff --git a/tests/spec/module.i b/tests/spec/module.c
similarity index 51%
rename from tests/spec/module.i
rename to tests/spec/module.c
index 3dbcb97724..abf32bb566 100644
--- a/tests/spec/module.i
+++ b/tests/spec/module.c
@@ -1,5 +1,6 @@
 /* run.config
    STDOPT:
+   STDOPT: +"-cpp-extra-args='-DILL_TYPED'"
  */
 
 /*@
@@ -19,3 +20,34 @@
   lemma AbsOp: \forall Foo::t x, integer n;
     B::opN(x,\abs(n)) == A::opN(x,\abs(n));
  */
+
+#ifdef ILL_TYPED
+
+/*@
+
+  import Foo \as F;
+  logic t x = F::e; // ill-formed: t should be F::t
+*/
+
+/*@
+  import Foo \as F;
+  import foo \as f;
+  logic F::t x = f::bar::inv(F::e); // OK
+  logic F::t y = bar::inv(F::e); // KO
+*/
+
+/*@
+  module A {
+     logic integer a = 0;
+     module B {
+       logic integer b = a + 1;
+     }
+  }
+
+import A::B \as b;
+
+logic integer z = b::a; // KO
+
+*/
+
+#endif
diff --git a/tests/spec/oracle/module.res.oracle b/tests/spec/oracle/module.0.res.oracle
similarity index 89%
rename from tests/spec/oracle/module.res.oracle
rename to tests/spec/oracle/module.0.res.oracle
index 0f5fca9d76..359107044c 100644
--- a/tests/spec/oracle/module.res.oracle
+++ b/tests/spec/oracle/module.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing module.i (no preprocessing)
+[kernel] Parsing module.c (with preprocessing)
 /* Generated by Frama-C */
 /*@
 module Foo {
diff --git a/tests/spec/oracle/module.1.res.oracle b/tests/spec/oracle/module.1.res.oracle
new file mode 100644
index 0000000000..85b7349dbe
--- /dev/null
+++ b/tests/spec/oracle/module.1.res.oracle
@@ -0,0 +1,46 @@
+[kernel] Parsing module.c (with preprocessing)
+[kernel:annot-error] module.c:29: Warning: 
+  no such type t. Ignoring global annotation
+[kernel:annot-error] module.c:36: Warning: 
+  unbound logic function bar::inv. Ignoring global annotation
+[kernel:annot-error] module.c:49: Warning: 
+  unbound logic variable b::a. Ignoring global annotation
+/* Generated by Frama-C */
+/*@
+module Foo {
+  type t;
+  
+  logic t e;
+  
+  logic t op(t x, t y) ;
+  
+  logic t opN(t x, ℤ n) = n ≥ 0? op(x, opN(x, n - 1)): e;
+  
+  }
+ */
+/*@
+module foo::bar {
+  logic Foo::t inv(Foo::t x) ;
+  
+  logic Foo::t opN(Foo::t x, ℤ n) =
+    n ≥ 0? Foo::opN(x, n): opN(inv(x), -n);
+  
+  }
+ */
+/*@
+lemma AbsOp:
+  ∀ Foo::t x, ℤ n; foo::bar::opN(x, \abs(n)) ≡ Foo::opN(x, \abs(n));
+ */
+/*@ logic Foo::t x= foo::bar::inv(Foo::e);
+ */
+/*@ module A {
+      logic ℤ a= 0;
+      
+      module B {
+        logic ℤ b= A::a + 1;
+        
+        }
+      
+      }
+ */
+
-- 
GitLab