diff options
| -rw-r--r-- | Test/Makefile | 17 | ||||
| -rw-r--r-- | Test/VSComp2010/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/alltests.txt | 8 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/Iter.dfy | 115 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 11 | ||||
| -rw-r--r-- | Test/runtest.bat | 39 | ||||
| -rw-r--r-- | Test/runtestall.bat | 24 | ||||
| -rw-r--r-- | Test/vacid0/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/vstte2012/runtest.bat | 4 |
14 files changed, 232 insertions, 14 deletions
diff --git a/Test/Makefile b/Test/Makefile new file mode 100644 index 00000000..92c67ae4 --- /dev/null +++ b/Test/Makefile @@ -0,0 +1,17 @@ +TESTS_FILE = alltests.txt +LONG = $(shell awk '{ if (tolower($$2) ~ /^long$$/) print $$1 }' $(TESTS_FILE)) +NORMAL = $(shell awk '{ if (tolower($$2) ~ /^use$$/) print $$1 }' $(TESTS_FILE)) +TESTS = $(NORMAL) + +all: dafny + +dafny: $(addprefix rundfy-, $(TESTS)) + +show: + @echo $(TESTS) + +long: + $(MAKE) TESTS="$(NORMAL) $(LONG)" all + +rundfy-%: + @if ls -f $*/*.dfy >/dev/null 2>&1 ; then cmd /c "runtest.bat $* $(FLAGS)" ; fi || : diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat index 63f5df23..9206f51e 100644 --- a/Test/VSComp2010/runtest.bat +++ b/Test/VSComp2010/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
Problem3-FindZero.dfy Problem4-Queens.dfy
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index f5b9d1b9..8f6dfc40 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
echo.
diff --git a/Test/alltests.txt b/Test/alltests.txt new file mode 100644 index 00000000..8ecf0e25 --- /dev/null +++ b/Test/alltests.txt @@ -0,0 +1,8 @@ +dafny0 Use Dafny functionality tests
+dafny1 Use Various Dafny examples
+dafny2 Use More Dafny examples
+dafny3 Use And more Dafny examples
+VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
+vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
+vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
+VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 9118e388..9ebf88ae 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
for %%f in (Simple.dfy) do (
echo.
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index a49bbf9a..60b562d0 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
for %%f in (Queue.dfy PriorityQueue.dfy
ExtensibleArray.dfy ExtensibleArrayAuto.dfy
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 72959830..126b6001 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
REM soon again: SnapshotableTrees.dfy
for %%f in (
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer new file mode 100644 index 00000000..3c339054 --- /dev/null +++ b/Test/dafny3/Answer @@ -0,0 +1,4 @@ +
+-------------------- Iter.dfy --------------------
+
+Dafny program verifier finished with 15 verified, 0 errors
diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy new file mode 100644 index 00000000..543a889a --- /dev/null +++ b/Test/dafny3/Iter.dfy @@ -0,0 +1,115 @@ +class List<T> {
+ ghost var Contents: seq<T>;
+ ghost var Repr: set<object>;
+
+ var a: array<T>;
+ var n: nat;
+
+ predicate Valid()
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr &&
+ a in Repr &&
+ n <= a.Length != 0 &&
+ Contents == a[..n]
+ }
+
+ constructor Init()
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ ensures Contents == [];
+ {
+ Contents, Repr, n := [], {this}, 0;
+ a := new T[25];
+ Repr := Repr + {a};
+ }
+
+ method Add(t: T)
+ requires Valid();
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == old(Contents) + [t];
+ {
+ if (n == a.Length) {
+ var b := new T[2 * a.Length];
+ parallel (i | 0 <= i < a.Length) {
+ b[i] := a[i];
+ }
+ assert b[..n] == a[..n] == Contents;
+ a, Repr := b, Repr + {b};
+ assert b[..n] == Contents;
+ }
+ a[n], n, Contents := t, n + 1, Contents + [t];
+ }
+}
+
+class Cell { var data: int; }
+
+iterator M<T>(l: List<T>, c: Cell) yields (x: T)
+ requires l != null && l.Valid() && c != null;
+ reads l.Repr;
+ modifies c;
+ yield requires true;
+ yield ensures xs <= l.Contents; // this is needed in order for the next line to be well-formed
+ yield ensures x == l.Contents[|xs|-1];
+ ensures xs == l.Contents;
+{
+ var i := 0;
+ while (i < l.n)
+ invariant i <= l.n && i == |xs| && xs <= l.Contents;
+ {
+ if (*) { assert l.Valid(); } // this property is maintained, due to the reads clause
+ if (*) {
+ x := l.a[i]; yield; // or, equivalently, 'yield l.a[i]'
+ i := i + 1;
+ } else {
+ x, i := l.a[i], i + 1;
+ yield;
+ }
+ }
+}
+
+method Client<T(==)>(l: List, stop: T) returns (s: seq<T>)
+ requires l != null && l.Valid();
+{
+ var c := new Cell;
+ var iter := new M.M(l, c);
+ s := [];
+ while (true)
+ invariant iter.Valid() && fresh(iter._new);
+ invariant iter.xs <= l.Contents;
+ decreases |l.Contents| - |iter.xs|;
+ {
+ var more := iter.MoveNext();
+ if (!more) { break; }
+ s := s + [iter.x];
+ if (iter.x == stop) { return; } // if we ever see 'stop', then just end
+ }
+}
+
+method PrintSequence<T>(s: seq<T>)
+{
+ var i := 0;
+ while (i < |s|)
+ {
+ print s[i], " ";
+ i := i + 1;
+ }
+ print "\n";
+}
+
+method Main()
+{
+ var myList := new List.Init();
+ var i := 0;
+ while (i < 100)
+ invariant myList.Valid() && fresh(myList.Repr);
+ {
+ myList.Add(i);
+ i := i + 2;
+ }
+ var s := Client(myList, 89);
+ PrintSequence(s);
+ s := Client(myList, 14);
+ PrintSequence(s);
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat new file mode 100644 index 00000000..a7b201e1 --- /dev/null +++ b/Test/dafny3/runtest.bat @@ -0,0 +1,11 @@ +@echo off
+setlocal
+
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
+
+for %%f in (Iter.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
+)
diff --git a/Test/runtest.bat b/Test/runtest.bat new file mode 100644 index 00000000..5b3d45ae --- /dev/null +++ b/Test/runtest.bat @@ -0,0 +1,39 @@ +@echo off
+rem Usage: runtest.bat <dir>
+if "%1" == "" goto noDirSpecified
+if not exist %1\nul goto noDirExists
+echo ----- Running regression test %1
+pushd %1
+if not exist runtest.bat goto noRunTest
+call runtest.bat -nologo -logPrefix:%* > Output
+rem There seem to be some race between finishing writing to the Output file, and running fc.
+rem Calling fc twice seems to fix (or at least alleviate) the problem.
+fc /W Answer Output > nul
+fc /W Answer Output > nul
+if not errorlevel 1 goto passTest
+echo %1 FAILED
+goto errorEnd
+
+:passTest
+echo %1 Succeeded
+goto end
+
+:noDirSpecified
+echo runtest: Error: Syntax: runtest testDirectory [ additionalTestArguments ... ]
+goto errorEnd
+
+:noDirExists
+echo runtest: Error: There is no test directory %1
+goto errorEnd
+
+:noRunTest
+echo runtest: Error: no runtest.bat found in test directory %1
+goto errorEnd
+
+:errorEnd
+popd
+exit /b 1
+
+:end
+popd
+exit /b 0
diff --git a/Test/runtestall.bat b/Test/runtestall.bat new file mode 100644 index 00000000..207bb030 --- /dev/null +++ b/Test/runtestall.bat @@ -0,0 +1,24 @@ +@echo off
+setlocal
+
+set errors=0
+
+if "%1" == "short" goto UseShort
+
+set IncludeLong=True
+goto Loop
+
+:UseShort
+set IncludeLong=False
+shift
+goto Loop
+
+:Loop
+for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1
+
+if not %IncludeLong%==True goto End
+
+for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Long call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1
+
+:End
+exit /b %errors%
\ No newline at end of file diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat index cd047d39..b7d5f4d8 100644 --- a/Test/vacid0/runtest.bat +++ b/Test/vacid0/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
echo.
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index 7f7c9b9f..c2236cf7 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -1,8 +1,8 @@ @echo off
setlocal
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES\Dafny.exe
for %%f in (
Two-Way-Sort.dfy
|