diff options
| author |  Rustan Leino <unknown> | 2014-02-28 18:29:55 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-28 18:29:55 -0800 |
| commit | efc11762c9d697aef9eae0cebd1d17aaf229d2a8 (patch) | |
| tree | 19aa11db720426ae6eb3c0989a4e5244aa428058 | |
| parent | a800b7c751757fc65a87bbffeb3ddc222d98a1a5 (diff) | |
Moved the (long running) CloudMake test files to their own directory
| -rw-r--r-- | Test/alltests.txt | 1 | ||||
| -rw-r--r-- | Test/cloudmake/Answer | 12 | ||||
| -rw-r--r-- | Test/cloudmake/CloudMake-CachedBuilds.dfy (renamed from Test/dafny4/CloudMake-CachedBuilds.dfy) | 0 | ||||
| -rw-r--r-- | Test/cloudmake/CloudMake-ConsistentBuilds.dfy (renamed from Test/dafny4/CloudMake-ConsistentBuilds.dfy) | 0 | ||||
| -rw-r--r-- | Test/cloudmake/CloudMake-ParallelBuilds.dfy (renamed from Test/dafny4/CloudMake-ParallelBuilds.dfy) | 0 | ||||
| -rw-r--r-- | Test/cloudmake/runtest.bat | 7 | ||||
| -rw-r--r-- | Test/dafny4/Answer | 12 | ||||
| -rw-r--r-- | Test/dafny4/runtest.bat | 2 |
8 files changed, 21 insertions, 13 deletions
diff --git a/Test/alltests.txt b/Test/alltests.txt index 6edb80fb..c586a561 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -3,6 +3,7 @@ dafny1 Use Various Dafny examples dafny2 Use More Dafny examples
dafny3 Use And more Dafny examples
dafny4 Use More, more, more!
+cloudmake Use CloudMake formalization and proofs
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
diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer new file mode 100644 index 00000000..3758853e --- /dev/null +++ b/Test/cloudmake/Answer @@ -0,0 +1,12 @@ +
+-------------------- CloudMake-ParallelBuilds.dfy --------------------
+
+Dafny program verifier finished with 244 verified, 0 errors
+
+-------------------- CloudMake-CachedBuilds.dfy --------------------
+
+Dafny program verifier finished with 104 verified, 0 errors
+
+-------------------- CloudMake-ConsistentBuilds.dfy --------------------
+
+Dafny program verifier finished with 59 verified, 0 errors
diff --git a/Test/dafny4/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy index f1150809..f1150809 100644 --- a/Test/dafny4/CloudMake-CachedBuilds.dfy +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy diff --git a/Test/dafny4/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy index dcfa1a2b..dcfa1a2b 100644 --- a/Test/dafny4/CloudMake-ConsistentBuilds.dfy +++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy diff --git a/Test/dafny4/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index e76f60d8..e76f60d8 100644 --- a/Test/dafny4/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat new file mode 100644 index 00000000..8fc7ccbb --- /dev/null +++ b/Test/cloudmake/runtest.bat @@ -0,0 +1,7 @@ +@echo off
+setlocal
+
+set BINARIES=..\..\Binaries
+set DAFNY_EXE=%BINARIES%\Dafny.exe
+
+%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy
diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer index 4a09a1d8..61eedf16 100644 --- a/Test/dafny4/Answer +++ b/Test/dafny4/Answer @@ -33,15 +33,3 @@ Dafny program verifier finished with 33 verified, 0 errors -------------------- Circ.dfy --------------------
Dafny program verifier finished with 16 verified, 0 errors
-
--------------------- CloudMake-ParallelBuilds.dfy --------------------
-
-Dafny program verifier finished with 244 verified, 0 errors
-
--------------------- CloudMake-CachedBuilds.dfy --------------------
-
-Dafny program verifier finished with 104 verified, 0 errors
-
--------------------- CloudMake-ConsistentBuilds.dfy --------------------
-
-Dafny program verifier finished with 59 verified, 0 errors
diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat index ea4869db..c6778179 100644 --- a/Test/dafny4/runtest.bat +++ b/Test/dafny4/runtest.bat @@ -4,4 +4,4 @@ setlocal set BINARIES=..\..\Binaries
set DAFNY_EXE=%BINARIES%\Dafny.exe
-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy
+%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy
|