Merge remote-tracking branch 'origin/develop'

k-distribution/tests/regression-new/checks/expandMacroEnsures.k

@@ -0,0 +1,13 @@
+// Copyright (c) K Team. All Rights Reserved.
+
+module EXPANDMACROENSURES
+    imports INT
+    imports BOOL
+
+    syntax Int  ::= #foo ( Int ) [function]
+    syntax Bool ::= #baz ( Int ) [alias]
+
+//    rule #baz ( X ) => X // NOTE I should be defined !!
+
+    rule #foo( X ) => X       ensures  #baz( X )
+endmodule

k-distribution/tests/regression-new/checks/expandMacroEnsures.k.out

@@ -0,0 +1,9 @@
+[Error] Compiler: Rule contains macro symbol that was not expanded
+	Source(expandMacroEnsures.k)
+	Location(12,10,12,49)
+	12 |	    rule #foo( X ) => X       ensures  #baz( X )
+	   .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 1 structural errors after macro expansion.
+  while executing phase "expand macros" on sentence at
+	Source(expandMacroEnsures.k)
+	Location(12,10,12,49)

k-distribution/tests/regression-new/checks/expandMacroRequires.k

@@ -0,0 +1,13 @@
+// Copyright (c) K Team. All Rights Reserved.
+
+module EXPANDMACROREQUIRES
+    imports INT
+    imports BOOL
+
+    syntax Int  ::= #foo ( Int ) [function]
+    syntax Bool ::= #bar ( Int ) [alias]
+
+//    rule #bar ( X ) => X >Int 0 // NOTE I should be defined !!
+
+    rule #foo( X ) => X       requires #bar( X )
+endmodule

k-distribution/tests/regression-new/checks/expandMacroRequires.k.out

@@ -0,0 +1,9 @@
+[Error] Compiler: Rule contains macro symbol that was not expanded
+	Source(expandMacroRequires.k)
+	Location(12,10,12,49)
+	12 |	    rule #foo( X ) => X       requires #bar( X )
+	   .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 1 structural errors after macro expansion.
+  while executing phase "expand macros" on sentence at
+	Source(expandMacroRequires.k)
+	Location(12,10,12,49)

kernel/src/main/java/org/kframework/compile/ExpandMacros.java

@@ -188,16 +188,20 @@ private Sentence check(Sentence s) {
          * contain macros that have not been expanded.
          */
         if (s instanceof RuleOrClaim){
-            new VisitK() {
+            VisitK visitor = new VisitK() {
                 @Override
                 public void apply(KApply k) {
                     Option<Att> atts = mod.attributesFor().get(k.klabel());
                     if (atts.isDefined() && mod.attributesFor().apply(k.klabel()).getMacro().isDefined()) {
                         errors.add(KEMException.compilerError("Rule contains macro symbol that was not expanded", s));
                     }
-                    k.klist().items().stream().forEach(i -> super.apply(i));
+                    k.klist().items().forEach(super::apply);
                 }
-            }.accept(((RuleOrClaim) s).body());
+            };
+
+            visitor.accept(((RuleOrClaim) s).body());
+            visitor.accept(((RuleOrClaim) s).requires());
+            visitor.accept(((RuleOrClaim) s).ensures());
         }
 
         if (!errors.isEmpty()) {