Chalice: Completely switch to new testing scripts (more flexible and fine-grained testing) and remove old test.bat. New testing scripts are described in Chalice/tests/readme.txt.

52 files changed, 114 insertions, 134 deletions

diff --git a/Chalice/test.bat b/Chalice/test.bat
deleted file mode 100644
index 4bf5db07..00000000
--- a/Chalice/test.bat
+++ /dev/null
@@ -1,46 +0,0 @@
-@echo off

-echo start > Output

-

-set CHALICE=call scala -cp bin chalice.Chalice -nologo 

-

-

-REM to do: AssociationList

-REM to do: GhostConst

-REM to do: Leaks -checkLeaks

-

-for %%f in (cell counter dining-philosophers ForkJoin HandOverHand

-            iterator iterator2 producer-consumer

-            prog0 prog1 prog2 prog3 prog4 ImplicitLocals

-            RockBand swap OwickiGries ProdConsChannel LoopLockChange

-            PetersonsAlgorithm quantifiers) do (

-  echo   Testing %%f.chalice ...

-  echo ------ Running regression test %%f.chalice >> Output

-  %CHALICE% %* examples\%%f.chalice >> Output 2>&1

-)

-

-echo   Testing cell-defaults.chalice ...

-echo ------ Running regression test cell-defaults.chalice >> Output

-%CHALICE% %* -defaults -autoFold -autoMagic examples\cell-defaults.chalice >> Output 2>&1

-

-echo   Testing RockBand-automagic.chalice ...

-echo ------ Running regression test RockBand-automagic.chalice >> Output

-%CHALICE% %* -defaults -autoMagic -checkLeaks -autoFold examples\RockBand-automagic.chalice >> Output 2>&1

-

-

-fc examples\Answer Output > nul

-if not errorlevel 1 goto passTest

-goto failTest

-

-:passTest

-echo Succeeded

-goto end

-

-:failTest

-echo Failed

-goto end

-

-:errorEnd

-exit /b 1

-

-:end

-exit /b 0

diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt
index 719af1af..618d878a 100644
--- a/Chalice/tests/examples/AssociationList.output.txt
+++ b/Chalice/tests/examples/AssociationList.output.txt
@@ -1,4 +1,4 @@
-Verification of AssociationList.chalice 

+Verification of AssociationList.chalice using parameters="" 

 

   19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu.

   64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.

diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt
index 46633611..4099f78a 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt
+++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt
@@ -1,4 +1,4 @@
-Verification of CopyLessMessagePassing-with-ack.chalice 

+Verification of CopyLessMessagePassing-with-ack.chalice using parameters="" 

 

 

 Boogie program verifier finished with 11 verified, 0 errors

diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt
index e8c42507..6ba69de5 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt
+++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt
@@ -1,4 +1,4 @@
-Verification of CopyLessMessagePassing-with-ack2.chalice 

+Verification of CopyLessMessagePassing-with-ack2.chalice using parameters="" 

 

 

 Boogie program verifier finished with 12 verified, 0 errors

diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt
index d6fd8be3..859c9998 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing.output.txt
+++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt
@@ -1,4 +1,4 @@
-Verification of CopyLessMessagePassing.chalice 

+Verification of CopyLessMessagePassing.chalice using parameters="" 

 

 

 Boogie program verifier finished with 11 verified, 0 errors

diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt
index 06d44bec..ed2abbda 100644
--- a/Chalice/tests/examples/ForkJoin.output.txt
+++ b/Chalice/tests/examples/ForkJoin.output.txt
@@ -1,4 +1,4 @@
-Verification of ForkJoin.chalice 

+Verification of ForkJoin.chalice using parameters="" 

 

 

 Boogie program verifier finished with 18 verified, 0 errors

diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt
index a57fe677..de7ab98c 100644
--- a/Chalice/tests/examples/HandOverHand.output.txt
+++ b/Chalice/tests/examples/HandOverHand.output.txt
@@ -1,4 +1,4 @@
-Verification of HandOverHand.chalice 

+Verification of HandOverHand.chalice using parameters="" 

 

 

 Boogie program verifier finished with 10 verified, 0 errors

diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/examples/ImplicitLocals.output.txt
index c3f518ed..4d7b08b1 100644
--- a/Chalice/tests/examples/ImplicitLocals.output.txt
+++ b/Chalice/tests/examples/ImplicitLocals.output.txt
@@ -1,4 +1,4 @@
-Verification of ImplicitLocals.chalice 

+Verification of ImplicitLocals.chalice using parameters="" 

 

 

 Boogie program verifier finished with 8 verified, 0 errors

diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt
index c6c69a24..7a03627f 100644
--- a/Chalice/tests/examples/LoopLockChange.output.txt
+++ b/Chalice/tests/examples/LoopLockChange.output.txt
@@ -1,4 +1,4 @@
-Verification of LoopLockChange.chalice 

+Verification of LoopLockChange.chalice using parameters="" 

 

   10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.

   35.5: The loop might lock/unlock more than the lockchange clause allows.

diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt
index ff585ab1..a56e7442 100644
--- a/Chalice/tests/examples/OwickiGries.output.txt
+++ b/Chalice/tests/examples/OwickiGries.output.txt
@@ -1,4 +1,4 @@
-Verification of OwickiGries.chalice 

+Verification of OwickiGries.chalice using parameters="" 

 

 

 Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt
index bf470e3a..5bc49aaa 100644
--- a/Chalice/tests/examples/PetersonsAlgorithm.output.txt
+++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt
@@ -1,4 +1,4 @@
-Verification of PetersonsAlgorithm.chalice 

+Verification of PetersonsAlgorithm.chalice using parameters="" 

 

 

 Boogie program verifier finished with 7 verified, 0 errors

diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt
index 1cfe7dfb..de5e8467 100644
--- a/Chalice/tests/examples/ProdConsChannel.output.txt
+++ b/Chalice/tests/examples/ProdConsChannel.output.txt
@@ -1,4 +1,4 @@
-Verification of ProdConsChannel.chalice 

+Verification of ProdConsChannel.chalice using parameters="" 

 

   47.3: Method body is not allowed to leave any debt.

   61.3: Method body is not allowed to leave any debt.

diff --git a/Chalice/tests/examples/RockBand-automagic.chalice b/Chalice/tests/examples/RockBand-automagic.chalice
index d231ae5a..8a64b691 100644
--- a/Chalice/tests/examples/RockBand-automagic.chalice
+++ b/Chalice/tests/examples/RockBand-automagic.chalice
@@ -1,3 +1,4 @@
+// chalice-parameter=-checkLeaks -defaults -autoFold -autoMagic

 // verify this program with -checkLeaks -defaults -autoFold -autoMagic

 

 class Client {

diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/examples/RockBand-automagic.output.txt
index d494e16a..9ce4b436 100644
--- a/Chalice/tests/examples/RockBand-automagic.output.txt
+++ b/Chalice/tests/examples/RockBand-automagic.output.txt
@@ -1,11 +1,8 @@
-Verification of RockBand-automagic.chalice 

+Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic" 

 

-  19.27: Location might not be readable.

-  27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.

-  41.10: Location might not be readable.

-  50.5: Location might not be writable

-  58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.

-  77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.

-  96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.

+  20.27: Location might not be readable.

+  28.3: Method RockBand.Init might leak references.

+  42.10: Location might not be readable.

+  51.5: Location might not be writable

 

-Boogie program verifier finished with 28 verified, 7 errors

+Boogie program verifier finished with 31 verified, 4 errors

diff --git a/Chalice/tests/examples/RockBand.chalice b/Chalice/tests/examples/RockBand.chalice
index 49b99a68..379b4113 100644
--- a/Chalice/tests/examples/RockBand.chalice
+++ b/Chalice/tests/examples/RockBand.chalice
@@ -1,3 +1,4 @@
+// chalice-parameter=-checkLeaks -defaults -autoFold

 // verify this program with -checkLeaks -defaults -autoFold

 

 class Client {

diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt
index 3fb1b1c6..a52b021b 100644
--- a/Chalice/tests/examples/RockBand.output.txt
+++ b/Chalice/tests/examples/RockBand.output.txt
@@ -1,10 +1,4 @@
-Verification of RockBand.chalice 

+Verification of RockBand.chalice using parameters="-checkLeaks -defaults -autoFold" 

 

-  27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.

-  41.10: Location might not be readable.

-  50.5: Location might not be writable

-  58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.

-  77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.

-  96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.

 

-Boogie program verifier finished with 29 verified, 6 errors

+Boogie program verifier finished with 35 verified, 0 errors

diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt
index b8b74b59..93271d87 100644
--- a/Chalice/tests/examples/Sieve.output.txt
+++ b/Chalice/tests/examples/Sieve.output.txt
@@ -1,4 +1,4 @@
-Verification of Sieve.chalice 

+Verification of Sieve.chalice using parameters="" 

 

 

 Boogie program verifier finished with 11 verified, 0 errors

diff --git a/Chalice/tests/examples/cell-defaults.chalice b/Chalice/tests/examples/cell-defaults.chalice
index 4781db97..eb826f89 100644
--- a/Chalice/tests/examples/cell-defaults.chalice
+++ b/Chalice/tests/examples/cell-defaults.chalice
@@ -1,3 +1,4 @@
+// chalice-parameter=-defaults -autoFold -autoMagic

 // verify this program with -defaults -autoFold -autoMagic

 

 class Cell module Library {

diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt
index ee7ae4e5..0f7a3b80 100644
--- a/Chalice/tests/examples/cell-defaults.output.txt
+++ b/Chalice/tests/examples/cell-defaults.output.txt
@@ -1,17 +1,7 @@
-Verification of cell-defaults.chalice 

+Verification of cell-defaults.chalice using parameters="-defaults -autoFold -autoMagic" 

 

-  6.3: The postcondition at 8.13 might not hold. Insufficient fraction at 8.13 for Cell.valid.

-  17.5: Location might not be writable

-  24.5: Location might not be writable

-  31.5: The field x of the target of the free statement might not be writable.

-  38.5: Location might not be readable.

-  52.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Interval.valid.

-  71.10: Location might not be readable.

-  80.10: Location might not be readable.

-  89.10: Location might not be readable.

-  96.5: Location might not be readable.

-  102.5: Location might not be readable.

-  107.5: Location might not be readable.

-  131.5: Assertion might not hold. Insufficient fraction at 131.12 for Cell.valid.

+  97.5: The heap of the callee might not be strictly smaller than the heap of the caller.

+  103.5: The heap of the callee might not be strictly smaller than the heap of the caller.

+  132.5: Assertion might not hold. Insufficient fraction at 132.12 for Cell.valid.

 

-Boogie program verifier finished with 19 verified, 13 errors

+Boogie program verifier finished with 29 verified, 3 errors

diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt
index 3ca21dd2..2c6c617d 100644
--- a/Chalice/tests/examples/cell.output.txt
+++ b/Chalice/tests/examples/cell.output.txt
@@ -1,4 +1,4 @@
-Verification of cell.chalice 

+Verification of cell.chalice using parameters="" 

 

   142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.

 

diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt
index 6fdd2d7c..961b1413 100644
--- a/Chalice/tests/examples/counter.output.txt
+++ b/Chalice/tests/examples/counter.output.txt
@@ -1,4 +1,4 @@
-Verification of counter.chalice 

+Verification of counter.chalice using parameters="" 

 

   69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.

   80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.

diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt
index 2bf72597..651bd638 100644
--- a/Chalice/tests/examples/dining-philosophers.output.txt
+++ b/Chalice/tests/examples/dining-philosophers.output.txt
@@ -1,4 +1,4 @@
-Verification of dining-philosophers.chalice 

+Verification of dining-philosophers.chalice using parameters="" 

 

 

 Boogie program verifier finished with 12 verified, 0 errors

diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt
index a03f7c0c..de361b94 100644
--- a/Chalice/tests/examples/iterator.output.txt
+++ b/Chalice/tests/examples/iterator.output.txt
@@ -1,4 +1,4 @@
-Verification of iterator.chalice 

+Verification of iterator.chalice using parameters="" 

 

 

 Boogie program verifier finished with 22 verified, 0 errors

diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt
index 512a2e26..af837e6f 100644
--- a/Chalice/tests/examples/iterator2.output.txt
+++ b/Chalice/tests/examples/iterator2.output.txt
@@ -1,4 +1,4 @@
-Verification of iterator2.chalice 

+Verification of iterator2.chalice using parameters="" 

 

 

 Boogie program verifier finished with 21 verified, 0 errors

diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt
index b164664d..65f03446 100644
--- a/Chalice/tests/examples/linkedlist.output.txt
+++ b/Chalice/tests/examples/linkedlist.output.txt
@@ -1,4 +1,4 @@
-Verification of linkedlist.chalice 

+Verification of linkedlist.chalice using parameters="" 

 

   49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.

 

diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt
index ebf7c738..b21044bb 100644
--- a/Chalice/tests/examples/producer-consumer.output.txt
+++ b/Chalice/tests/examples/producer-consumer.output.txt
@@ -1,4 +1,4 @@
-Verification of producer-consumer.chalice 

+Verification of producer-consumer.chalice using parameters="" 

 

 

 Boogie program verifier finished with 36 verified, 0 errors

diff --git a/Chalice/tests/examples/prog0.output.txt b/Chalice/tests/examples/prog0.output.txt
index 7949fa88..5b329874 100644
--- a/Chalice/tests/examples/prog0.output.txt
+++ b/Chalice/tests/examples/prog0.output.txt
@@ -1,4 +1,4 @@
-Verification of prog0.chalice 

+Verification of prog0.chalice using parameters="" 

 

 The program did not typecheck.

 3.17: undeclared member a in class C

diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt
index eb552ac2..61938bf7 100644
--- a/Chalice/tests/examples/prog1.output.txt
+++ b/Chalice/tests/examples/prog1.output.txt
@@ -1,4 +1,4 @@
-Verification of prog1.chalice 

+Verification of prog1.chalice using parameters="" 

 

   9.10: Location might not be readable.

   25.5: Location might not be writable

diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt
index 1581039d..b3ea3e93 100644
--- a/Chalice/tests/examples/prog2.output.txt
+++ b/Chalice/tests/examples/prog2.output.txt
@@ -1,4 +1,4 @@
-Verification of prog2.chalice 

+Verification of prog2.chalice using parameters="" 

 

   24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.

   31.13: Location might not be readable.

diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/examples/prog3.output.txt
index 7537f222..82eeab18 100644
--- a/Chalice/tests/examples/prog3.output.txt
+++ b/Chalice/tests/examples/prog3.output.txt
@@ -1,4 +1,4 @@
-Verification of prog3.chalice 

+Verification of prog3.chalice using parameters="" 

 

   76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.

   76.3: Method might lock/unlock more than allowed.

diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt
index 950c2277..62197afb 100644
--- a/Chalice/tests/examples/prog4.output.txt
+++ b/Chalice/tests/examples/prog4.output.txt
@@ -1,4 +1,4 @@
-Verification of prog4.chalice 

+Verification of prog4.chalice using parameters="" 

 

   5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.

   17.7: The target of the release statement might not be locked by the current thread.

diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt
index 20b0af7b..efae2ed6 100644
--- a/Chalice/tests/examples/quantifiers.output.txt
+++ b/Chalice/tests/examples/quantifiers.output.txt
@@ -1,4 +1,4 @@
-Verification of quantifiers.chalice 

+Verification of quantifiers.chalice using parameters="" 

 

   57.29: The heap of the callee might not be strictly smaller than the heap of the caller.

 

diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt
index 29df3021..70bac3a2 100644
--- a/Chalice/tests/examples/swap.output.txt
+++ b/Chalice/tests/examples/swap.output.txt
@@ -1,4 +1,4 @@
-Verification of swap.chalice 

+Verification of swap.chalice using parameters="" 

 

 

 Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt
index 510ae7f5..9d92923a 100644
--- a/Chalice/tests/permission-model/basic.output.txt
+++ b/Chalice/tests/permission-model/basic.output.txt
@@ -1,4 +1,4 @@
-Verification of basic.chalice 

+Verification of basic.chalice using parameters="" 

 

   28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.

   48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.

diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt
index 11543925..a79b5fb1 100644
--- a/Chalice/tests/permission-model/channels.output.txt
+++ b/Chalice/tests/permission-model/channels.output.txt
@@ -1,4 +1,4 @@
-Verification of channels.chalice 

+Verification of channels.chalice using parameters="" 

 

   8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f.

   18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f.

diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt
index c1167c3b..98cd0d4e 100644
--- a/Chalice/tests/permission-model/locks.output.txt
+++ b/Chalice/tests/permission-model/locks.output.txt
@@ -1,4 +1,4 @@
-Verification of locks.chalice 

+Verification of locks.chalice using parameters="" 

 

   21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.

   24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.

diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt
index fd3c0a76..6754cf7f 100644
--- a/Chalice/tests/permission-model/peculiar.output.txt
+++ b/Chalice/tests/permission-model/peculiar.output.txt
@@ -1,4 +1,4 @@
-Verification of peculiar.chalice 

+Verification of peculiar.chalice using parameters="" 

 

   35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x.

 

diff --git a/Chalice/tests/permission-model/permarith_parser.output.txt b/Chalice/tests/permission-model/permarith_parser.output.txt
index f124b714..bc6598a1 100644
--- a/Chalice/tests/permission-model/permarith_parser.output.txt
+++ b/Chalice/tests/permission-model/permarith_parser.output.txt
@@ -1,4 +1,4 @@
-Verification of permarith_parser.chalice 

+Verification of permarith_parser.chalice using parameters="" 

 

 The program did not typecheck.

 6.14: fraction in permission must be of type integer

diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt
index f735cf85..afbd9be7 100644
--- a/Chalice/tests/permission-model/permission_arithmetic.output.txt
+++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt
@@ -1,4 +1,4 @@
-Verification of permission_arithmetic.chalice 

+Verification of permission_arithmetic.chalice using parameters="" 

 

   24.5: Assertion might not hold. The permission at 24.18 might not be positive.

   40.5: The precondition at 33.14 might not hold. The permission at 33.20 might not be positive.

diff --git a/Chalice/tests/permission-model/predicate_error1.output.txt b/Chalice/tests/permission-model/predicate_error1.output.txt
index d7964c29..a5e27bac 100644
--- a/Chalice/tests/permission-model/predicate_error1.output.txt
+++ b/Chalice/tests/permission-model/predicate_error1.output.txt
@@ -1,3 +1,3 @@
-Verification of predicate_error1.chalice 

+Verification of predicate_error1.chalice using parameters="" 

 

 Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.

diff --git a/Chalice/tests/permission-model/predicate_error2.output.txt b/Chalice/tests/permission-model/predicate_error2.output.txt
index cc580b7b..fb660013 100644
--- a/Chalice/tests/permission-model/predicate_error2.output.txt
+++ b/Chalice/tests/permission-model/predicate_error2.output.txt
@@ -1,3 +1,3 @@
-Verification of predicate_error2.chalice 

+Verification of predicate_error2.chalice using parameters="" 

 

 Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.

diff --git a/Chalice/tests/permission-model/predicate_error3.output.txt b/Chalice/tests/permission-model/predicate_error3.output.txt
index 3e325f1b..9f5b503c 100644
--- a/Chalice/tests/permission-model/predicate_error3.output.txt
+++ b/Chalice/tests/permission-model/predicate_error3.output.txt
@@ -1,3 +1,3 @@
-Verification of predicate_error3.chalice 

+Verification of predicate_error3.chalice using parameters="" 

 

 Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.

diff --git a/Chalice/tests/permission-model/predicate_error4.output.txt b/Chalice/tests/permission-model/predicate_error4.output.txt
index 8cd03821..16da656f 100644
--- a/Chalice/tests/permission-model/predicate_error4.output.txt
+++ b/Chalice/tests/permission-model/predicate_error4.output.txt
@@ -1,3 +1,3 @@
-Verification of predicate_error4.chalice 

+Verification of predicate_error4.chalice using parameters="" 

 

 Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.

diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt
index be87e044..30c08a1a 100644
--- a/Chalice/tests/permission-model/predicates.output.txt
+++ b/Chalice/tests/permission-model/predicates.output.txt
@@ -1,4 +1,4 @@
-Verification of predicates.chalice 

+Verification of predicates.chalice using parameters="" 

 

   37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x.

   55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x.

diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt
index 1ff1d596..863e79d8 100644
--- a/Chalice/tests/permission-model/scaling.output.txt
+++ b/Chalice/tests/permission-model/scaling.output.txt
@@ -1,4 +1,4 @@
-Verification of scaling.chalice 

+Verification of scaling.chalice using parameters="" 

 

   33.5: Assertion might not hold. Insufficient fraction at 33.12 for Cell.x.

   36.3: The postcondition at 38.13 might not hold. Insufficient fraction at 38.13 for Cell.read1.

diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt
index 16dd9137..c7099103 100644
--- a/Chalice/tests/permission-model/sequences.output.txt
+++ b/Chalice/tests/permission-model/sequences.output.txt
@@ -1,4 +1,4 @@
-Verification of sequences.chalice 

+Verification of sequences.chalice using parameters="" 

 

   36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f

   60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f

diff --git a/Chalice/tests/readme.txt b/Chalice/tests/readme.txt
index 0e09fb57..be0b6f91 100644
--- a/Chalice/tests/readme.txt
+++ b/Chalice/tests/readme.txt
@@ -31,9 +31,9 @@ Commands (sorted by relevance):
   current directory.

 - getboogieoutput.bat: File used internally by generete_reference.bat.

 

+To provide additional parameters to Chalice when verifying the tests (e.g., to

+test the autoMagic feature, see tests/examples/RockBand-automagic.chalice), one

+can start the Chalice source file with the line

+  "// chalice-parameter=<list of space-separated parameters>"

 

-Note: There is also an alternative way to execute the tests in example, namely

-to use the script test.bat. The scripts in test-scripts allow more fine-grained

-testing, but they do not allow to use special parameters for certain tests

-(e.g. -autoMagic).

-For the refinement tests, there is a bash script test.sh, similar to test.bat.

+Note: For the refinement tests, there is a bash script test.sh.

diff --git a/Chalice/tests/test-scripts/generate_reference.bat b/Chalice/tests/test-scripts/generate_reference.bat
index a2e9c443..0c480e5c 100644
--- a/Chalice/tests/test-scripts/generate_reference.bat
+++ b/Chalice/tests/test-scripts/generate_reference.bat
@@ -1,5 +1,4 @@
 @echo off

-

 set getboogieoutput="%~dp0\getboogieoutput.bat"

 

 echo   Generating reference for %1.chalice ...

diff --git a/Chalice/tests/test-scripts/generate_reference_all.bat b/Chalice/tests/test-scripts/generate_reference_all.bat
index 83b04700..1e9e7cfb 100644
--- a/Chalice/tests/test-scripts/generate_reference_all.bat
+++ b/Chalice/tests/test-scripts/generate_reference_all.bat
@@ -1,10 +1,9 @@
 @echo off

 

-set getboogieoutput="%~dp0\getboogieoutput.bat"

+set generatereference="%~dp0\generate_reference.bat"

 

 for /F %%f in ('dir *.chalice /b') do (

-  echo   Generating reference for %%~nf.chalice ...

-  call %getboogieoutput% %%~nf %1 %2 %3 %4 %5 %6 %7

+  call %generatereference% %%~nf %1 %2 %3 %4 %5 %6 %7

 )

 

 exit /b 0

diff --git a/Chalice/tests/test-scripts/getboogieoutput.bat b/Chalice/tests/test-scripts/getboogieoutput.bat
index eb7d99a4..40590120 100644
--- a/Chalice/tests/test-scripts/getboogieoutput.bat
+++ b/Chalice/tests/test-scripts/getboogieoutput.bat
@@ -1,13 +1,33 @@
 @echo off

-

 set chalice="%~dp0\..\..\chalice.bat"

+set getparams="%~dp0\getparams.bat"

 

 set output="%1.output.txt"

 

-echo Verification of %1.chalice > %output%

+:: get parameters

+set chaliceparameters=

+setlocal EnableDelayedExpansion

+set done=0

+set key=a

+FOR /F "usebackq tokens=1,2 delims==" %%i in (%1.chalice) do (

+    

+    if !done!==0 (

+        set key=%%i

+        set param=%%j

+    )

+    

+    set done=1

+)

+set str=// chalice-parameter

+if "!key!"=="!str!" (

+    set chaliceparameters=!param!

+)

+

+echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%

 echo.>> %output%

-call %chalice% "%1.chalice" %2 %3 %4 %5 >> %output% 2>&1

+call %chalice% "%1.chalice" %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1

 

 set o=%~dp1%out.bpl

 if exist "%o%" copy "%o%" "%1.bpl">nul

 if exist "%o%" del "%~dp1%out.bpl"

+goto :eof

diff --git a/Chalice/tests/test-scripts/reg_test.bat b/Chalice/tests/test-scripts/reg_test.bat
index d31773da..0e5e4dbf 100644
--- a/Chalice/tests/test-scripts/reg_test.bat
+++ b/Chalice/tests/test-scripts/reg_test.bat
@@ -1,15 +1,34 @@
 @echo off

-

+setlocal

 set chalice="%~dp0\..\..\chalice.bat"

 set diff="%~dp0\diff.bat"

 

 if not exist "%1.chalice" goto errorNotFound

 if not exist "%1.output.txt" goto errorNoRef

 

+:: get parameters

+set chaliceparameters=

+setlocal EnableDelayedExpansion

+set done=0

+set key=a

+FOR /F "usebackq tokens=1,2 delims==" %%i in (%1.chalice) do (

+    

+    if !done!==0 (

+        set key=%%i

+        set param=%%j

+    )

+    

+    set done=1

+)

+set str=// chalice-parameter

+if "!key!"=="!str!" (

+    set chaliceparameters=!param!

+)

+

 set output=output.txt

-echo Verification of %1.chalice > %output%

+echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%

 echo.>> %output%

-call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1

+call %chalice% "%1.chalice" %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1

 

 fc "%1.output.txt" output.txt > nul

 if not errorlevel 1 goto passTest

@@ -27,11 +46,13 @@ goto errorEnd
 :errorEnd

 if exist out.bpl del out.bpl

 if exist output.txt del output.txt

+endlocal

 exit /b 1

 

 :end

 if exist out.bpl del out.bpl

 if exist output.txt del output.txt

+endlocal

 exit /b 0

 

 :errorNotFound

diff --git a/Chalice/tests/test-scripts/test.bat b/Chalice/tests/test-scripts/test.bat
index 321fdcef..3908ae68 100644
--- a/Chalice/tests/test-scripts/test.bat
+++ b/Chalice/tests/test-scripts/test.bat
@@ -1,13 +1,16 @@
 @echo off

 

 set chalice="%~dp0\..\..\chalice.bat"

+set getparams="%~dp0\getparams.bat"

 

 if not exist "%1.chalice" goto errorNotFound

 

 set output=output.txt

-echo Verification of %1.chalice > %output%

+set chaliceparameters=

+call %getparams% %1 chaliceparameters

+echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%

 echo.>> %output%

-call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1

+call %chalice% "%1.chalice" %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1

 type %output%

 

 exit /B 0