10 files changed, 98 insertions, 35 deletions
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 30c3eefd..70f9bbd0 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -57,6 +57,7 @@ class C {
   }
 
   method A5()
+    decreases *;
   {
     var a := new CP<int,C>;
     var b := new CP<int,object>;
diff --git a/Test/dafny0/DTypes.dfy.expect b/Test/dafny0/DTypes.dfy.expect
index fccf1c9a..9b4288e9 100644
--- a/Test/dafny0/DTypes.dfy.expect
+++ b/Test/dafny0/DTypes.dfy.expect
@@ -1,5 +1,5 @@
-DTypes.dfy(181,3): Error BP5003: A postcondition might not hold on this return path.
-DTypes.dfy(180,15): Related location: This is the postcondition that might not hold.
+DTypes.dfy(182,3): Error BP5003: A postcondition might not hold on this return path.
+DTypes.dfy(181,15): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
 DTypes.dfy(18,14): Error: assertion violation
@@ -8,20 +8,20 @@ Execution trace:
 DTypes.dfy(56,18): Error: assertion violation
 Execution trace:
     (0,0): anon0
-DTypes.dfy(120,13): Error: assertion violation
-DTypes.dfy(92,30): Related location
+DTypes.dfy(121,13): Error: assertion violation
+DTypes.dfy(93,30): Related location
 Execution trace:
     (0,0): anon0
-DTypes.dfy(126,13): Error: assertion violation
-DTypes.dfy(92,20): Related location
+DTypes.dfy(127,13): Error: assertion violation
+DTypes.dfy(93,20): Related location
 Execution trace:
     (0,0): anon0
-DTypes.dfy(136,12): Error: assertion violation
-DTypes.dfy(131,6): Related location
-DTypes.dfy(92,20): Related location
+DTypes.dfy(137,12): Error: assertion violation
+DTypes.dfy(132,6): Related location
+DTypes.dfy(93,20): Related location
 Execution trace:
     (0,0): anon0
-DTypes.dfy(157,12): Error: assertion violation
+DTypes.dfy(158,12): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect
index dd53a883..b269e3b2 100644
--- a/Test/dafny0/Modules1.dfy.expect
+++ b/Test/dafny0/Modules1.dfy.expect
@@ -11,6 +11,7 @@ Execution trace:
     (0,0): anon0
     (0,0): anon3_Else
 Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0
+Modules1.dfy(54,13): Related location
 Execution trace:
     (0,0): anon0
 Modules1.dfy(62,3): Error: failure to decrease termination measure
diff --git a/Test/dafny0/RealCompare.dfy.expect b/Test/dafny0/RealCompare.dfy.expect
index aca50548..e0f70fc0 100644
--- a/Test/dafny0/RealCompare.dfy.expect
+++ b/Test/dafny0/RealCompare.dfy.expect
@@ -3,6 +3,7 @@ Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
 RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0
+RealCompare.dfy(48,13): Related location
 Execution trace:
     (0,0): anon0
 RealCompare.dfy(141,12): Error: assertion violation
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;
+  }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b6ebe5dc..4827dc07 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -134,7 +134,7 @@ ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
 ResolutionErrors.dfy(263,2): Error: duplicate label
 ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
 ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(292,4): Error: a constructor is allowed to be called only when an object is being allocated
 ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
 ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
 ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
@@ -176,4 +176,6 @@ ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from
 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
 ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-178 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+180 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TailCalls.dfy b/Test/dafny0/TailCalls.dfy
index ba683679..0bc282a4 100644
--- a/Test/dafny0/TailCalls.dfy
+++ b/Test/dafny0/TailCalls.dfy
@@ -30,25 +30,24 @@ method C(q: int) returns (x: int)
 }
 
 method D(q: int) returns (x: int)
-  decreases *;  // error: not allowed, because the method is not tail recursive
 {
   x := D(q-1);
   x := x + 1;
 }
 
-method E0(q: int) returns (x: int)
-  decreases *;  // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)
+method {:tailrecursion} E0(q: int) returns (x: int)  // error: not allowed, because the method is not
+  // tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)
 {
   x := E1(q-1);
 }
-method E1(q: int) returns (x: int)
-  decreases *;  // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)
+method {:tailrecursion} E1(q: int) returns (x: int)  // error: not allowed, because the method is not
+  // tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)
 {
   x := E0(q);
 }
 
 method F0(q: int) returns (x: int)
-  decreases *;  // fine, but no 'decreases' spec is needed at all here
+  decreases *;  // fine
 {
   x := D(q);
 }
@@ -63,18 +62,18 @@ method {:tailrecursion} G0(q: int) returns (x: int)
 {
   x := D(q);
 }
-method {:tailrecursion false} G1(q: int) returns (x: int)
-  decreases *;  // error: even though there is no recursion in this method's body, the annotation specifically says "not tail recursive", so (the easiest thing to do in the Resolver was to) generate an error
+method {:tailrecursion false} G1(q: int) returns (x: int)  // the annotation tells the compiler not to tail-call optimize
+  decreases *;
 {
-  x := D(q);
+  x := G1(q);
 }
 
 method H0(q: int) returns (x: int)
-  decreases *;  // fine, but no 'decreases' spec is needed at all here
+  decreases *;  // fine
 method {:tailrecursion} H1(q: int) returns (x: int)
-  decreases *;  // fine, but no 'decreases' spec is needed at all here
+  decreases *;  // fine
 method H2(q: int) returns (x: int)
-  decreases 5;  // fine, but no 'decreases' spec is needed at all here
+  decreases 5;  // fine
 
 class {:autocontracts} MyAutoContractClass {
   var left: MyAutoContractClass;
diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect
index 7fc51902..dc1eec5b 100644
--- a/Test/dafny0/TailCalls.dfy.expect
+++ b/Test/dafny0/TailCalls.dfy.expect
@@ -1,6 +1,4 @@
 TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
-TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods
-5 resolution/type errors detected in TailCalls.dfy
+TailCalls.dfy(38,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
+TailCalls.dfy(43,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
+3 resolution/type errors detected in TailCalls.dfy
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 377865fe..70c30aa6 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -275,6 +275,7 @@ function Zipper2<T>(a: List<T>, b: List<T>): List<T>
 
 method WhileStar0(n: int)
   requires 2 <= n;
+  decreases *;
 {
   var m := n;
   var k := 0;
@@ -429,3 +430,22 @@ class C {
     }
   }
 }
+
+// --------------------- decreases * tests
+
+module TerminationRefinement0 {
+  method M(x: int)
+    decreases *;
+  {
+    M(x);  // error [in TerminationRefinement1]: bad recursion
+           // Note, no complaint is issued in TerminationRefinement0, since
+           // the method is declared with 'decreases *'.
+  }
+}
+module TerminationRefinement1 refines TerminationRefinement0 {
+  method M...
+    decreases 4;  // this will cause termination checking to be done, and it will produce an error message for the recursive call
+  {
+    ...;
+  }
+}
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index b050c7de..ef8ee72e 100644
--- a/Test/dafny0/Termination.dfy.expect
+++ b/Test/dafny0/Termination.dfy.expect
@@ -1,4 +1,7 @@
-Termination.dfy(359,47): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](440,5): Error: failure to decrease termination measure
+Execution trace:
+    (0,0): anon0
+Termination.dfy(360,47): Error: failure to decrease termination measure
 Execution trace:
     (0,0): anon0
     (0,0): anon7_Else
@@ -44,12 +47,12 @@ Execution trace:
     (0,0): anon6_Else
     (0,0): anon7_Else
     (0,0): anon8_Then
-Termination.dfy(294,3): Error: decreases expression might not decrease
+Termination.dfy(295,3): Error: decreases expression might not decrease
 Execution trace:
-    Termination.dfy(294,3): anon9_LoopHead
+    Termination.dfy(295,3): anon9_LoopHead
     (0,0): anon9_LoopBody
-    Termination.dfy(294,3): anon10_Else
-    Termination.dfy(294,3): anon11_Else
+    Termination.dfy(295,3): anon10_Else
+    Termination.dfy(295,3): anon11_Else
     (0,0): anon12_Else
 
-Dafny program verifier finished with 59 verified, 7 errors
+Dafny program verifier finished with 62 verified, 8 errors