From c8ecf7cb50cc9405f4f52fec5449f0f38152cac9 Mon Sep 17 00:00:00 2001 From: Marco Antognini Date: Wed, 14 Dec 2016 16:19:29 +0100 Subject: [PATCH] Move some tests around - Aliasing3 is disabled because it make verification crash (see #289) - Aliasing4 is disabled because it make verification produce incorrect counter-example (see #287) - Inheritance9 is disabled because it make xlang crash (see #288) - UsingConcreteCLasses is enabled because verification is easy --- .../regression/genc/{valid => unverified}/Aliasing3.scala | 0 .../regression/genc/{valid => unverified}/Aliasing4.scala | 0 .../regression/genc/{valid => unverified}/Inheritance9.scala | 0 .../regression/genc/{valid => unverified}/LinearSearch.scala | 0 .../genc/{unverified => valid}/UsingConcreteClasses.scala | 2 +- 5 files changed, 1 insertion(+), 1 deletion(-) rename src/test/resources/regression/genc/{valid => unverified}/Aliasing3.scala (100%) rename src/test/resources/regression/genc/{valid => unverified}/Aliasing4.scala (100%) rename src/test/resources/regression/genc/{valid => unverified}/Inheritance9.scala (100%) rename src/test/resources/regression/genc/{valid => unverified}/LinearSearch.scala (100%) rename src/test/resources/regression/genc/{unverified => valid}/UsingConcreteClasses.scala (93%) diff --git a/src/test/resources/regression/genc/valid/Aliasing3.scala b/src/test/resources/regression/genc/unverified/Aliasing3.scala similarity index 100% rename from src/test/resources/regression/genc/valid/Aliasing3.scala rename to src/test/resources/regression/genc/unverified/Aliasing3.scala diff --git a/src/test/resources/regression/genc/valid/Aliasing4.scala b/src/test/resources/regression/genc/unverified/Aliasing4.scala similarity index 100% rename from src/test/resources/regression/genc/valid/Aliasing4.scala rename to src/test/resources/regression/genc/unverified/Aliasing4.scala diff --git a/src/test/resources/regression/genc/valid/Inheritance9.scala b/src/test/resources/regression/genc/unverified/Inheritance9.scala similarity index 100% rename from src/test/resources/regression/genc/valid/Inheritance9.scala rename to src/test/resources/regression/genc/unverified/Inheritance9.scala diff --git a/src/test/resources/regression/genc/valid/LinearSearch.scala b/src/test/resources/regression/genc/unverified/LinearSearch.scala similarity index 100% rename from src/test/resources/regression/genc/valid/LinearSearch.scala rename to src/test/resources/regression/genc/unverified/LinearSearch.scala diff --git a/src/test/resources/regression/genc/unverified/UsingConcreteClasses.scala b/src/test/resources/regression/genc/valid/UsingConcreteClasses.scala similarity index 93% rename from src/test/resources/regression/genc/unverified/UsingConcreteClasses.scala rename to src/test/resources/regression/genc/valid/UsingConcreteClasses.scala index 8725a6e20..434c01d3f 100644 --- a/src/test/resources/regression/genc/unverified/UsingConcreteClasses.scala +++ b/src/test/resources/regression/genc/valid/UsingConcreteClasses.scala @@ -13,7 +13,7 @@ object UsingConcreteClasses { if (child.opt.v == 42) 0 else 1 - } + } ensuring { _ == 0 } @extern def main(args: Array[String]): Unit = _main()