diff options
author | Rustan Leino <unknown> | 2013-12-13 17:43:35 -0800 |
---|---|---|
committer | Rustan Leino <unknown> | 2013-12-13 17:43:35 -0800 |
commit | 3caf3b4c9932ee60ce93b52cc229db7722f28278 (patch) | |
tree | 01c9f8a0971f8e1fd416ee11083cffc758f31899 | |
parent | bec9ceeba29e8513a41a65be5a8fdba8d68333e3 (diff) |
Produce "tail recursive" hover text in the IDE only for methods that are recursive
-rw-r--r-- | .hgignore | 1 | ||||
-rw-r--r-- | Source/Dafny/DafnyOptions.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 5 |
3 files changed, 6 insertions, 2 deletions
@@ -4,6 +4,7 @@ syntax: regexp ^Source/.*\.(smt2|bpl)$
^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$
Test/.*/Output
+Test/desktop/.*
Test/([^/]*)/([^/]*)\.sx
syntax: glob
*.exe
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 753fbb32..b69a9536 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -97,7 +97,7 @@ namespace Microsoft.Dafny ps.GetNumericArgument(ref InductionHeuristic, 7);
return true;
- case "noInclude":
+ case "noIncludes":
DisallowIncludes = true;
return true;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2e4c0c00..4c354e6a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1560,7 +1560,10 @@ namespace Microsoft.Dafny var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
if (status != TailRecursionStatus.NotTailRecursive) {
m.IsTailRecursive = true;
- ReportAdditionalInformation(m.tok, "tail recursive", m.Name.Length);
+ if (tailCall != null) {
+ // this means there was at least one recursive call
+ ReportAdditionalInformation(m.tok, "tail recursive", m.Name.Length);
+ }
}
}
}
|