add test

runtimeverification · May 28, 2020 · 4572df4 · 4572df4
1 parent d77e977
commit 4572df4
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 0 deletions.
diff --git a/k-distribution/tests/regression-new/checkWarns/Makefile b/k-distribution/tests/regression-new/checkWarns/Makefile
@@ -0,0 +1,4 @@
+KOMPILE_FLAGS=-w2e
+KOMPILE_BACKEND=llvm
+
+include ../../../include/kframework/ktest-fail.mak
diff --git a/k-distribution/tests/regression-new/checkWarns/checkUnusedVar.k b/k-distribution/tests/regression-new/checkWarns/checkUnusedVar.k
@@ -0,0 +1,13 @@
+module CHECKUNUSEDVAR-SYNTAX
+
+endmodule
+
+module CHECKUNUSEDVAR
+  imports INT
+
+  syntax KItem ::= foo(Int)
+
+  rule foo(X) => 0
+  rule foo(0) => !_:Int
+
+endmodule
diff --git a/k-distribution/tests/regression-new/checkWarns/checkUnusedVar.k.out b/k-distribution/tests/regression-new/checkWarns/checkUnusedVar.k.out
@@ -0,0 +1,3 @@
+[Error] Compiler: Variable 'X' defined but not used.
+	Source(checkUnusedVar.k)
+	Location(10,12,10,13)