diff options
-rw-r--r-- | Dafny/Dafny.atg | 6 | ||||
-rw-r--r-- | Dafny/Parser.cs | 6 | ||||
-rw-r--r-- | Dafny/Resolver.cs | 6 | ||||
-rw-r--r-- | Test/dafny1/Answer | 4 | ||||
-rw-r--r-- | Test/dafny1/runtest.bat | 2 | ||||
-rw-r--r-- | Test/dafny2/Answer | 4 | ||||
-rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 15 | ||||
-rw-r--r-- | Test/dafny2/runtest.bat | 3 | ||||
-rw-r--r-- | Test/vstte2012/Answer | 4 | ||||
-rw-r--r-- | Test/vstte2012/runtest.bat | 3 |
10 files changed, 37 insertions, 16 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index bfce5122..7d49fb8f 100644 --- a/Dafny/Dafny.atg +++ b/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/Dafny/Parser.cs b/Dafny/Parser.cs index 9ad05d3b..f585476d 100644 --- a/Dafny/Parser.cs +++ b/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/Dafny/Resolver.cs b/Dafny/Resolver.cs index 098bcc2e..c3eccb51 100644 --- a/Dafny/Resolver.cs +++ b/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
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index b2876948..06cac03b 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -11,6 +11,10 @@ Dafny program verifier finished with 24 verified, 0 errors Dafny program verifier finished with 11 verified, 0 errors
+-------------------- ExtensibleArrayAuto.dfy --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
+
-------------------- BinaryTree.dfy --------------------
Dafny program verifier finished with 24 verified, 0 errors
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 22bef761..fa7f7c70 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
for %%f in (Queue.dfy PriorityQueue.dfy
- ExtensibleArray.dfy
+ ExtensibleArray.dfy ExtensibleArrayAuto.dfy
BinaryTree.dfy
UnboundedStack.dfy
SeparationLogicList.dfy
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index f359e416..f466d813 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -27,6 +27,10 @@ Dafny program verifier finished with 4 verified, 0 errors Dafny program verifier finished with 23 verified, 0 errors
+-------------------- StoreAndRetrieve.dfy --------------------
+
+Dafny program verifier finished with 22 verified, 0 errors
+
-------------------- Intervals.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index 15c82d65..9ea7a3ff 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -1,4 +1,5 @@ -ghost module A imports Library {
+ghost module A {
+ module L = Library;
class {:autocontracts} StoreAndRetrieve<Thing> {
ghost var Contents: set<Thing>;
predicate Valid
@@ -13,12 +14,12 @@ ghost module A imports Library { {
Contents := Contents + {t};
}
- method Retrieve(matchCriterion: Function) returns (thing: Thing)
- requires exists t :: t in Contents && Function.Apply(matchCriterion, t);
+ method Retrieve(matchCriterion: L.Function) returns (thing: Thing)
+ requires exists t :: t in Contents && L.Function.Apply(matchCriterion, t);
ensures Contents == old(Contents);
- ensures thing in Contents && Function.Apply(matchCriterion, thing);
+ ensures thing in Contents && L.Function.Apply(matchCriterion, thing);
{
- var k :| k in Contents && Function.Apply(matchCriterion, k);
+ var k :| k in Contents && L.Function.Apply(matchCriterion, k);
thing := k;
}
}
@@ -44,9 +45,9 @@ module B refines A { var i := 0;
while (i < |arr|)
invariant i < |arr|;
- invariant forall j :: 0 <= j < i ==> !Function.Apply(matchCriterion, arr[j]);
+ invariant forall j :: 0 <= j < i ==> !L.Function.Apply(matchCriterion, arr[j]);
{
- if (Function.Apply(matchCriterion, arr[i])) { break; }
+ if (L.Function.Apply(matchCriterion, arr[i])) { break; }
i := i + 1;
}
var k := arr[i];
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 19b116d2..25dbed54 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -4,7 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-REM soon again: SnapshotableTrees.dfy StoreAndRetrieve.dfy
+REM soon again: SnapshotableTrees.dfy
for %%f in (
Classics.dfy
TreeBarrier.dfy
@@ -13,6 +13,7 @@ for %%f in ( COST-verif-comp-2011-2-MaxTree-datatype.dfy
COST-verif-comp-2011-3-TwoDuplicates.dfy
COST-verif-comp-2011-4-FloydCycleDetect.dfy
+ StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
) do (
diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer index 15a95de1..bca270c3 100644 --- a/Test/vstte2012/Answer +++ b/Test/vstte2012/Answer @@ -11,6 +11,10 @@ Dafny program verifier finished with 25 verified, 0 errors Dafny program verifier finished with 13 verified, 0 errors
+-------------------- RingBufferAuto.dfy --------------------
+
+Dafny program verifier finished with 13 verified, 0 errors
+
-------------------- Tree.dfy --------------------
Dafny program verifier finished with 15 verified, 0 errors
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index cda455fa..7f7c9b9f 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -4,11 +4,10 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-REM removed for now: RingBufferAuto.dfy
for %%f in (
Two-Way-Sort.dfy
Combinators.dfy
- RingBuffer.dfy
+ RingBuffer.dfy RingBufferAuto.dfy
Tree.dfy
BreadthFirstSearch.dfy
) do (
|