Some invalid tests are actually supported by Leon/GenC!

epfl-lara · Sep 21, 2016 · 0f1e15a · 0f1e15a
1 parent 7f06782
commit 0f1e15a
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 6 deletions.
diff --git a/...ession/genc/invalid/BadInheritance2.scala → .../regression/genc/valid/Inheritance7.scala b/...ession/genc/invalid/BadInheritance2.scala → .../regression/genc/valid/Inheritance7.scala
@@ -3,10 +3,10 @@
 import leon.annotation.extern
 import leon.lang._
 
-object BadInheritance2 {
+object Inheritance7 {
 
   abstract class Base {
-    def get: Int // Defining abstract method is not supported
+    def get: Int // Defining abstract method IS supported
   }
 
   case class Derived1(x: Int) extends Base {
@@ -17,8 +17,11 @@ object BadInheritance2 {
     override def get: Int = 1
   }
 
+  def test1 = Derived1(42).get     // == 0
+  def test2 = Derived2(58).get - 1 // == 0
+
   def _main() = {
-    0
+    test1 + test2
   } ensuring { _ == 0 }
 
   @extern

diff --git a/...ession/genc/invalid/BadInheritance1.scala → .../regression/genc/valid/Inheritance8.scala b/...ession/genc/invalid/BadInheritance1.scala → .../regression/genc/valid/Inheritance8.scala
@@ -3,7 +3,7 @@
 import leon.annotation.extern
 import leon.lang._
 
-object BadInheritance1 {
+object Inheritance8 {
 
   abstract class Base {
     def get: Int = 1
@@ -12,11 +12,14 @@ object BadInheritance1 {
   case class Derived1(x: Int) extends Base
 
   case class Derived2(x: Int) extends Base {
-    override def get: Int = 0 // Overriding a method is not supported
+    override def get: Int = 0 // Overriding a method IS supported
   }
 
+  def test1 = Derived1(42).get - 1 // == 0
+  def test2 = Derived2(58).get     // == 0
+
   def _main() = {
-    0
+    test1 + test2
   } ensuring { _ == 0 }
 
   @extern