diff --git a/k-distribution/tests/regression-new/checkWarns/Makefile b/k-distribution/tests/regression-new/checkWarns/Makefile new file mode 100644 index 00000000000..7133790b2e6 --- /dev/null +++ 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 new file mode 100644 index 00000000000..3a2961b9925 --- /dev/null +++ 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 new file mode 100644 index 00000000000..c8d12e1840c --- /dev/null +++ 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)