From f235dfbc792bb885f3c76e4267658c1a9ef838d8 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 7 Jul 2015 15:27:58 -0700
Subject: Fixed crashes in overrides checking of function decreases clauses,
 and improved the error message reported to users

---
 Test/dafny0/Trait/TraitsDecreases.dfy | 46 +++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

(limited to 'Test/dafny0/Trait/TraitsDecreases.dfy')

diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy
index 53ce28be..8ab3672a 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy
@@ -106,3 +106,49 @@ class CC extends TT {
     decreases *
   { }
 }
+
+
+// The following module contains various regression tests
+module More {
+  trait A0 {
+    predicate P() decreases 5
+  }
+  class B0 extends A0 {
+    predicate P()  // error: rank is not lower
+  }
+
+  trait A1 {
+    predicate P() decreases 5
+  }
+  class B1 extends A1 {
+    predicate P() reads this  // error: rank is not lower
+  }
+
+  trait A2 {
+    predicate P(x: int)
+  }
+  class B2 extends A2 {
+    predicate P(x: int) reads this  // error: rank is not lower
+  }
+
+  trait A3 {
+    predicate P() reads this
+  }
+  class B3 extends A3 {
+    predicate P()  // error: rank is not lower
+  }
+
+  trait A4 {
+    predicate P(x: int) decreases 5
+  }
+  class B4 extends A4 {
+    predicate P(x: int)  // error: rank is not lower
+  }
+
+  trait A5 {
+    method M(x: int) decreases 5
+  }
+  class B5 extends A5 {
+    method M(x: int)  // error: rank is not lower
+  }
+}
-- 
cgit v1.2.3