diff --git a/run-tests.sh b/run-tests.sh index f1e606a6e76685d6911359614424fe53b01b34d9..cedaea2d3ec3e75c79161e5a33ac3225368a372d 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -1,6 +1,6 @@ -#!/bin/sh +#!/bin/bash -nbtests=$(ls -l testcases/regression/*valid/*.scala | wc -l) +nbtests=$(ls -l testcases/regression/{valid,invalid,error}/*.scala | wc -l) nbsuccess=0 failedtests="" @@ -26,6 +26,17 @@ for f in testcases/regression/invalid/*.scala; do fi done +for f in testcases/regression/error/*.scala; do + echo -n "Running $f, expecting ERROR, got: " + res=`./leon --timeout=5 --oneline "$f"` + echo $res | tr [a-z] [A-Z] + if [ $res = error ]; then + nbsuccess=$((nbsuccess + 1)) + else + failedtests="$failedtests $f" + fi +done + echo "$nbsuccess out of $nbtests tests were successful" if [ $nbtests -eq $nbsuccess ]; then echo "PASSED" diff --git a/testcases/regression/error/InstanceOf1.scala b/testcases/regression/error/InstanceOf1.scala new file mode 100644 index 0000000000000000000000000000000000000000..a1974b4bcf8c92f320f8357297536a6053c11b98 --- /dev/null +++ b/testcases/regression/error/InstanceOf1.scala @@ -0,0 +1,23 @@ +object InstanceOf1 { + + abstract class A + case class B(i: Int) extends A + case class C(i: Int) extends A + + abstract class Z + case class Y(i: Int) extends Z + + def foo(): Int = { + //require(3.isInstanceOf[Int]) + val b: A = B(2) + if(b.isInstanceOf[Y]) + 0 + else + -1 + } ensuring(_ == 0) + + def bar(): Int = foo() + +} + +// vim: set ts=4 sw=4 et: diff --git a/testcases/regression/valid/InstanceOf1.scala b/testcases/regression/valid/InstanceOf1.scala new file mode 100644 index 0000000000000000000000000000000000000000..1c52338bbda859f82ef7ea619af088b9c1a1812d --- /dev/null +++ b/testcases/regression/valid/InstanceOf1.scala @@ -0,0 +1,18 @@ +object InstanceOf1 { + + abstract class A + case class B(i: Int) extends A + case class C(i: Int) extends A + + def foo(): Int = { + require(C(3).isInstanceOf[C]) + val b: A = B(2) + if(b.isInstanceOf[B]) + 0 + else + -1 + } ensuring(_ == 0) + + def bar(): Int = foo() + +}