diff options
| author |  Jason Koenig <unknown> | 2012-07-02 11:51:44 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-02 11:51:44 -0700 |
| commit | a4729bac8fd4a4df88e539f187d1ec4984bec471 (patch) | |
| tree | 5a544a77bcf154a45d9bff429a84556ec8f0d862 /Source/Dafny | |
| parent | 3cc4fef8f9715ca93de2d40448cc9690813e1383 (diff) | |
Dafny: reinstated autocontracts
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 6 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 6 |
3 files changed, 13 insertions, 5 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index bfce5122..7d49fb8f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -778,7 +778,11 @@ UpdateStmt<out Statement/*!*/ s> (. if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
- s = new UpdateStmt(x, lhss, rhss);
+ if (lhss.Count == 0 && rhss.Count == 0) {
+ s = new BlockStmt(x, new List<Statement>()); // error, give empty statement
+ } else {
+ s = new UpdateStmt(x, lhss, rhss);
+ }
}
.)
.
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 9ad05d3b..f585476d 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1297,7 +1297,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
- s = new UpdateStmt(x, lhss, rhss);
+ if (lhss.Count == 0 && rhss.Count == 0) {
+ s = new BlockStmt(x, new List<Statement>()); // error, give empty statement
+ } else {
+ s = new UpdateStmt(x, lhss, rhss);
+ }
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 098bcc2e..c3eccb51 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -141,7 +141,7 @@ namespace Microsoft.Dafny { var refinementTransformer = new RefinementTransformer(this);
- //Rewriter rewriter = new AutoContractsRewriter();
+ IRewriter rewriter = new AutoContractsRewriter();
var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
foreach (var decl in sortedDecls) {
if (decl is LiteralModuleDecl) {
@@ -155,7 +155,7 @@ namespace Microsoft.Dafny { // by the bodies.
var literalDecl = (LiteralModuleDecl)decl;
var m = (literalDecl).ModuleDef;
- //rewriter.PreResolve(m);
+ rewriter.PreResolve(m);
ModuleSignature refinedSig = null;
if (m.RefinementBaseRoot != null) {
if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out refinedSig)) {
@@ -182,7 +182,7 @@ namespace Microsoft.Dafny { refinementTransformer.PostResolve(m);
// give rewriter a chance to do processing
- //rewriter.PostResolve(m);
+ rewriter.PostResolve(m);
} else if (decl is AliasModuleDecl) {
var alias = (AliasModuleDecl)decl;
// resolve the path
|