diff options
| author |  Rustan Leino <unknown> | 2013-08-02 19:55:40 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-02 19:55:40 -0700 |
| commit | 41f1a6131273ca0900d03a7adfaec96443a2cb2f (patch) | |
| tree | fba65e7a7b9139cf9100d7b827d7f0026faafe56 /Source/Dafny/Resolver.cs | |
| parent | 46492ad1f93fdacf488eecd1abbc8c86371d4a56 (diff) | |
| parent | 6625a9607810fb1d76b964109f2f7a8a71d43d04 (diff) | |
Merge adjustments
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0fb2b3bb..8162eacd 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1566,7 +1566,7 @@ namespace Microsoft.Dafny var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
if (status != TailRecursionStatus.NotTailRecursive) {
m.IsTailRecursive = true;
- ReportAddionalInformation(m.tok, "is tail recursive", m.Name.Length);
+ ReportAddionalInformation(m.tok, "tail recursive", m.Name.Length);
}
}
}
@@ -4035,17 +4035,19 @@ namespace Microsoft.Dafny ResolveExpression(e0, true, codeContext);
Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression
for (int i = 1; i < s.Lines.Count; i++) {
- var e1 = s.Lines[i];
- ResolveExpression(e1, true, codeContext);
- Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e0.Type, e1.Type)) {
- Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
- } else {
- var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
- ResolveExpression(step, true, codeContext);
- s.Steps.Add(step);
+ if (i < s.Lines.Count - 1 || prevErrorCount == ErrorCount) { // do not resolve the dummy step if there were errors, it might generate more errors
+ var e1 = s.Lines[i];
+ ResolveExpression(e1, true, codeContext);
+ Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e0.Type, e1.Type)) {
+ Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
+ } else {
+ var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
+ ResolveExpression(step, true, codeContext);
+ s.Steps.Add(step);
+ }
+ e0 = e1;
}
- e0 = e1;
}
// clear the labels for the duration of checking the hints, because break statements are not allowed to leave a forall statement
|