Fixed crashes in overrides checking of function decreases clauses, and improved the error message reported to users

1 files changed, 2 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 134fb4c1..d14d82a3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2223,6 +2223,7 @@ namespace Microsoft.Dafny {
   public interface ICallable : ICodeContext

   {

     IToken Tok { get; }

+    string WhatKind { get; }

     string NameRelativeToModule { get; }

     Specification<Expression> Decreases { get; }

     /// <summary>

@@ -2234,6 +2235,7 @@ namespace Microsoft.Dafny {
   }

   public class DontUseICallable : ICallable

   {

+    public string WhatKind { get { throw new cce.UnreachableException(); } }

     public bool IsGhost { get { throw new cce.UnreachableException(); } }

     public List<TypeParameter> TypeArgs { get { throw new cce.UnreachableException(); } }

     public List<Formal> Ins { get { throw new cce.UnreachableException(); } }