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
epfl-lara · Jan 25, 2017 · 1e76e46 · 1e76e46
1 parent 5df0c98
commit 1e76e46
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 1 deletion.
diff --git a/...ces/regression/genc/valid/Aliasing3.scala → ...egression/genc/unverified/Aliasing3.scala b/...ces/regression/genc/valid/Aliasing3.scala → ...egression/genc/unverified/Aliasing3.scala
diff --git a/...ces/regression/genc/valid/Aliasing4.scala → ...egression/genc/unverified/Aliasing4.scala b/...ces/regression/genc/valid/Aliasing4.scala → ...egression/genc/unverified/Aliasing4.scala
diff --git a/.../regression/genc/valid/Inheritance9.scala → ...ession/genc/unverified/Inheritance9.scala b/.../regression/genc/valid/Inheritance9.scala → ...ession/genc/unverified/Inheritance9.scala
diff --git a/.../regression/genc/valid/LinearSearch.scala → ...ession/genc/unverified/LinearSearch.scala b/.../regression/genc/valid/LinearSearch.scala → ...ession/genc/unverified/LinearSearch.scala
diff --git a/...enc/unverified/UsingConcreteClasses.scala → ...ion/genc/valid/UsingConcreteClasses.scala b/...enc/unverified/UsingConcreteClasses.scala → ...ion/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()
-Original file line number
+Diff line change
@@ Expand Up / @@ -13,7 +13,7 @@ object UsingConcreteClasses { @@
         if (child.opt.v == 42) 0
         else 1
-      }
+      } ensuring { _ == 0 }
       @extern
       def main(args: Array[String]): Unit = _main()
@@ Expand Down @@