Merge

1 files changed, 38 insertions, 0 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e0c37e2a..3c9156dd 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1121,3 +1121,41 @@ method IntegerDivision(s: set<bool>)
 {

   var t := s / s;  // error: / cannot be used with sets

 }

+

+// ----- decreases * tests ----

+

+method NonTermination_A()

+{

+  NonTermination_B();  // error: to call a non-terminating method, the caller must be marked 'decreases *'

+}

+

+method NonTermination_B()

+  decreases *;

+{

+  while true

+    decreases *;

+  {

+  }

+}

+

+method NonTermination_C()

+{

+  while true

+    decreases *;  // error: to use an infinite loop, the enclosing method must be marked 'decreases *'

+  {

+  }

+}

+

+method NonTermination_D()

+  decreases *;

+{

+  var n := 0;

+  while n < 100  // note, no 'decreases *' here, even if the nested loop may fail to terminate

+  {

+    while *

+      decreases *;

+    {

+    }

+    n := n + 1;

+  }

+}