diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-10 20:14:42 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 20:14:42 -0800 |
| commit | 84a1bd8c27e6eba3e3e10c1aa351feb781903c76 (patch) | |
| tree | 5158f5e257eb9973a2aef66a5ac95855269b471f /Source/Dafny | |
| parent | abf344ec3eafdbe0da2be591f6e45adc09217e1b (diff) | |
Dafny: fixed bugs in contract types, and a code bug that caused a contract to fail
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 6 |
2 files changed, 6 insertions, 5 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 088ca9d9..3d0492a8 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3306,8 +3306,9 @@ namespace Microsoft.Dafny { call = null;
int nonCallArguments = e.Arguments == null ? e.Tokens.Count : e.Tokens.Count - 1;
for (; p < nonCallArguments; p++) {
- r = ResolvePredicateOrField(e.Tokens[p], r, e.Tokens[p].val);
- if (r != null) {
+ var resolved = ResolvePredicateOrField(e.Tokens[p], r, e.Tokens[p].val);
+ if (resolved != null) {
+ r = resolved;
ResolveExpression(r, twoState);
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 27880f9d..0e928e4e 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3114,7 +3114,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(condition != null);
Contract.Requires(errorMessage != null);
- Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
if (RefinementToken.IsInherited(tok, currentModule)) {
// produce an assume instead
@@ -3131,7 +3131,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(errorMessage != null);
Contract.Requires(condition != null);
- Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
if (RefinementToken.IsInherited(tok, currentModule)) {
// produce a "skip" instead
@@ -3150,7 +3150,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(errorMessage != null);
Contract.Requires(condition != null);
- Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
if (RefinementToken.IsInherited(tok, currentModule)) {
// produce an assume instead
|