[tests] add some negative tests regarding scope resolution

tests/spec/module.i → tests/spec/module.c

 /* 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

tests/spec/oracle/module.res.oracle → tests/spec/oracle/module.0.res.oracle

-[kernel] Parsing module.i (no preprocessing)
+[kernel] Parsing module.c (with preprocessing)
 /* Generated by Frama-C */
 /*@
 module Foo {

tests/spec/oracle/module.1.res.oracle

+[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;
+        
+        }
+      
+      }
+ */
+