diff options
| author |  chmaria <unknown> | 2012-06-12 04:34:14 +0200 |
|---|---|---|
| committer | chmaria <unknown> | 2012-06-12 04:34:14 +0200 |
| commit | b4fa8bffd5db8bc5a68faf8f3b1f3587ce813f23 (patch) | |
| tree | 9b6952edef293fee8304e905474fec11196094ac | |
| parent | 2e803d553c8f579891a97a0c666e8b29044ff9d0 (diff) | |
Dafny: Added tests.
30 files changed, 1259 insertions, 29 deletions
diff --git a/Dafny/DafnyOptions.cs b/Dafny/DafnyOptions.cs index c0f8ea7a..cb126446 100644 --- a/Dafny/DafnyOptions.cs +++ b/Dafny/DafnyOptions.cs @@ -33,6 +33,7 @@ namespace Microsoft.Dafny public bool Compile = true;
public bool ForceCompile = false;
public bool SpillTargetCode = false;
+ public bool Verification = true;
public bool RuntimeChecking = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
@@ -91,6 +92,14 @@ namespace Microsoft.Dafny ps.GetNumericArgument(ref InductionHeuristic, 7);
return true;
+ case "verification":
+ int verification = 1; // 1 is default, verification
+ if (ps.GetNumericArgument(ref verification, 2))
+ {
+ Verification = verification == 1;
+ }
+ return true;
+
case "runtimeChecking":
int runtimeChecking = 0; // 0 is default, no runtime checking
if (ps.GetNumericArgument(ref runtimeChecking, 2))
@@ -157,6 +166,9 @@ namespace Microsoft.Dafny 1,2,3,4,5 - levels in between, ordered as follows as far as
how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6
6 (default) - most discriminating
+ /verification:<n>
+ 0 - do not verify the Dafny program
+ 1 (default) - verify the Dafny program
/runtimeChecking:<n>
0 (default) - ignore Dafny specifications during compilation
1 - translate Dafny specifications to CodeContracts during
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 34288d21..2f7175f4 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -151,7 +151,7 @@ namespace Microsoft.Dafny if (err != null) {
exitValue = ExitValue.DAFNY_ERROR;
ErrorWriteLine(err);
- } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck && DafnyOptions.O.Verification) {
Dafny.Translator translator = new Dafny.Translator();
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
if (CommandLineOptions.Clo.PrintFile != null)
@@ -188,6 +188,14 @@ namespace Microsoft.Dafny }
exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED;
}
+ else if (!DafnyOptions.O.Verification)
+ {
+ if (DafnyOptions.O.ForceCompile)
+ {
+ CompileDafnyProgram(dafnyProgram, fileNames[0]);
+ }
+ exitValue = ExitValue.NOT_VERIFIED;
+ }
}
return exitValue;
}
diff --git a/Test/VSComp2010/AnswerNoRuntimeChecking b/Test/VSComp2010/AnswerNoRuntimeChecking new file mode 100644 index 00000000..d0492caf --- /dev/null +++ b/Test/VSComp2010/AnswerNoRuntimeChecking @@ -0,0 +1,15 @@ +
+-------------------- Problem1-SumMax --------------------
+Compiled assembly into Problem1-SumMax.exe
+
+-------------------- Problem2-Invert --------------------
+Compiled assembly into Problem2-Invert.exe
+
+-------------------- Problem3-FindZero --------------------
+Compiled assembly into Problem3-FindZero.exe
+
+-------------------- Problem4-Queens --------------------
+Compiled assembly into Problem4-Queens.exe
+
+-------------------- Problem5-DoubleEndedQueue --------------------
+Compiled assembly into Problem5-DoubleEndedQueue.dll
diff --git a/Test/VSComp2010/AnswerRuntimeChecking b/Test/VSComp2010/AnswerRuntimeChecking new file mode 100644 index 00000000..858b6370 --- /dev/null +++ b/Test/VSComp2010/AnswerRuntimeChecking @@ -0,0 +1,4 @@ +
+-------------------- Problem1-SumMax --------------------
+Compiled assembly into Problem1-SumMax.exe
+Rewrote assembly into Problem1-SumMax.exe
diff --git a/Test/VSComp2010/runtestNoRuntimeChecking.bat b/Test/VSComp2010/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..4efd244a --- /dev/null +++ b/Test/VSComp2010/runtestNoRuntimeChecking.bat @@ -0,0 +1,28 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (Problem1-SumMax Problem2-Invert Problem3-FindZero
+ Problem4-Queens Problem5-DoubleEndedQueue) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/VSComp2010/runtestRuntimeChecking.bat b/Test/VSComp2010/runtestRuntimeChecking.bat new file mode 100644 index 00000000..d3b8a733 --- /dev/null +++ b/Test/VSComp2010/runtestRuntimeChecking.bat @@ -0,0 +1,33 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM Problem2-Invert : quantifiers
+REM Problem3-FindZero : ghost state
+REM Problem4-Queens : quantifiers
+REM Problem5-DoubleEndedQueue: ghost state
+
+for %%f in (Problem1-SumMax) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking index debe2cd3..81ac67ef 100644 --- a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking +++ b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking @@ -1,48 +1,31 @@ -------------------- b1 --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
Compiled assembly into b1.exe
-------------------- b2 --------------------
-
-Dafny program verifier finished with 6 verified, 0 errors
Compiled assembly into b2.exe
-------------------- b3 --------------------
-b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.
-
-Dafny program verifier finished with 9 verified, 1 error
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
-------------------- b4 --------------------
-
-Dafny program verifier finished with 11 verified, 0 errors
Compiled assembly into b4.dll
-------------------- b5 --------------------
-
-Dafny program verifier finished with 22 verified, 0 errors
Compiled assembly into b5.dll
-------------------- b6 --------------------
-
-Dafny program verifier finished with 21 verified, 0 errors
Compiled assembly into b6.exe
-------------------- b7 --------------------
-
-Dafny program verifier finished with 23 verified, 0 errors
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
Compilation error: Method _default.Client.Sort has no body
-------------------- b8 --------------------
-
-Dafny program verifier finished with 42 verified, 0 errors
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking index 841a04cf..49a440db 100644 --- a/Test/VSI-Benchmarks/AnswerRuntimeChecking +++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking @@ -1,29 +1,20 @@ -------------------- b1 --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
Compiled assembly into b1.exe
Rewrote assembly into b1.exe
-------------------- b3 --------------------
-b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.
-
-Dafny program verifier finished with 9 verified, 1 error
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
-------------------- b7 --------------------
-
-Dafny program verifier finished with 23 verified, 0 errors
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
Compilation error: Method _default.Client.Sort has no body
-------------------- b8 --------------------
-
-Dafny program verifier finished with 42 verified, 0 errors
Compilation error: Method _default.Queue.Init has no body
Compilation error: Method _default.Queue.Enqueue has no body
Compilation error: Method _default.Queue.Dequeue has no body
diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat index ccf1ffa8..c85b7606 100644 --- a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat +++ b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat @@ -8,7 +8,7 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe for %%f in (b1 b2 b3 b4 b5 b6 b7 b8) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /nologo /errorTrace:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
if exist %%f.cs. (
del %%f.cs
)
diff --git a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat index 8ac0f707..27df70a3 100644 --- a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat +++ b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat @@ -14,7 +14,7 @@ REM b6: functions for %%f in (b1 b3 b7 b8) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /nologo /errorTrace:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
if exist %%f.cs. (
del %%f.cs
)
diff --git a/Test/dafny0/AnswerNoRuntimeChecking b/Test/dafny0/AnswerNoRuntimeChecking new file mode 100644 index 00000000..04ece8ae --- /dev/null +++ b/Test/dafny0/AnswerNoRuntimeChecking @@ -0,0 +1,328 @@ +
+-------------------- Simple --------------------
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+
+-------------------- TypeTests --------------------
+TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
+TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
+TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+34 resolution/type errors detected in TypeTests.dfy
+
+-------------------- NatTypes --------------------
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+
+-------------------- SmallTests --------------------
+Compilation error: an assume statement cannot be compiled (line 13)
+Compilation error: compilation of seq<object> is not supported; consider introducing a ghost
+Compilation error: compilation of seq<object> is not supported; consider introducing a ghost
+Compilation error: compilation of seq<object> is not supported; consider introducing a ghost
+Compilation error: an assume statement cannot be compiled (line 545)
+Compilation error: an assume statement cannot be compiled (line 554)
+Compilation error: an assume statement cannot be compiled (line 556)
+Compilation error: an assume statement cannot be compiled (line 559)
+Compilation error: an assume statement cannot be compiled (line 571)
+Compilation error: an assume statement cannot be compiled (line 574)
+Compilation error: an assume statement cannot be compiled (line 575)
+Compilation error: an assume statement cannot be compiled (line 577)
+Compilation error: an assume statement cannot be compiled (line 584)
+Compilation error: an assume statement cannot be compiled (line 590)
+Compilation error: an assume statement cannot be compiled (line 596)
+Compilation error: an assume statement cannot be compiled (line 603)
+
+-------------------- Definedness --------------------
+Compilation error: an assume statement cannot be compiled (line 93)
+
+-------------------- FunctionSpecifications --------------------
+Compiled assembly into FunctionSpecifications.dll
+
+-------------------- ResolutionErrors --------------------
+ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
+ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)
+ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(261,2): Error: duplicate label
+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+48 resolution/type errors detected in ResolutionErrors.dfy
+
+-------------------- ParseErrors --------------------
+ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
+ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
+ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
+ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
+8 parse errors detected in ParseErrors.dfy
+
+-------------------- Array --------------------
+Compilation error: Arbitrary type ('B') cannot be compiled
+
+-------------------- MultiDimArray --------------------
+Compiled assembly into MultiDimArray.dll
+
+-------------------- NonGhostQuantifiers --------------------
+NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+20 resolution/type errors detected in NonGhostQuantifiers.dfy
+
+-------------------- AdvancedLHS --------------------
+Compiled assembly into AdvancedLHS.dll
+
+-------------------- ModulesCycle --------------------
+ModulesCycle.dfy(12,7): Error: module T named among imports does not exist
+ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G
+2 resolution/type errors detected in ModulesCycle.dfy
+
+-------------------- Modules0 --------------------
+Modules0.dfy(5,8): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
+Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
+Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(250,15): Error: unresolved identifier: X
+Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(294,16): Error: member R does not exist in class B
+Modules0.dfy(294,6): Error: expected method call, found expression
+Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
+30 resolution/type errors detected in Modules0.dfy
+
+-------------------- BadFunction --------------------
+Compiled assembly into BadFunction.dll
+
+-------------------- Comprehensions --------------------
+Compiled assembly into Comprehensions.exe
+
+-------------------- Basics --------------------
+Compilation error: an assume statement cannot be compiled (line 22)
+
+-------------------- ControlStructures --------------------
+Compiled assembly into ControlStructures.dll
+
+-------------------- DTypes --------------------
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+
+-------------------- ParallelResolveErrors --------------------
+ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field
+ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement
+ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement
+ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements
+ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement
+ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations
+15 resolution/type errors detected in ParallelResolveErrors.dfy
+
+-------------------- Parallel --------------------
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+Compilation error: an assume statement cannot be compiled (line 47)
+
+-------------------- TypeParameters --------------------
+Compiled assembly into TypeParameters.exe
+
+-------------------- Coinductive --------------------
+Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+4 resolution/type errors detected in Coinductive.dfy
+
+-------------------- Corecursion --------------------
+Compiled assembly into Corecursion.dll
+
+-------------------- TypeAntecedents --------------------
+Compiled assembly into TypeAntecedents.exe
+
+-------------------- SplitExpr --------------------
+Compiled assembly into SplitExpr.dll
+
+-------------------- LoopModifies --------------------
+Compiled assembly into LoopModifies.dll
+
+-------------------- Refinement --------------------
+Compilation error: Method BodyFree._default.M has no body
+Compilation error: an assume statement cannot be compiled (line 128)
+
+-------------------- RefinementErrors --------------------
+RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions
+RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause
+RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate
+RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base
+RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F
+RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')
+RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')
+RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')
+RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')
+RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines
+RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G
+11 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- ReturnErrors --------------------
+ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
+ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.
+3 resolution/type errors detected in ReturnErrors.dfy
+
+-------------------- ChainingDisjointTests --------------------
+Compiled assembly into ChainingDisjointTests.dll
+
+-------------------- CallStmtTests --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
+
+-------------------- MultiSets --------------------
+Compiled assembly into MultiSets.dll
+
+-------------------- PredExpr --------------------
+Compiled assembly into PredExpr.dll
+
+-------------------- LetExpr --------------------
+Compilation error: an assume statement cannot be compiled (line 31)
+Compilation error: an assume statement cannot be compiled (line 33)
+Compilation error: an assume statement cannot be compiled (line 34)
+
+-------------------- Skeletons --------------------
+Compilation error: an assume statement cannot be compiled (line 5)
+Compilation error: an assume statement cannot be compiled (line 7)
+
+-------------------- Maps --------------------
+Compiled assembly into Maps.exe
+
+-------------------- Compilation --------------------
+Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/AnswerRuntimeChecking b/Test/dafny0/AnswerRuntimeChecking new file mode 100644 index 00000000..e3970b78 --- /dev/null +++ b/Test/dafny0/AnswerRuntimeChecking @@ -0,0 +1,272 @@ +
+-------------------- Simple --------------------
+Compilation error: compilation of set<object> is not supported; consider introducing a ghost
+
+-------------------- TypeTests --------------------
+TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
+TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
+TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
+TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+34 resolution/type errors detected in TypeTests.dfy
+
+-------------------- NatTypes --------------------
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost
+
+-------------------- Definedness --------------------
+Compiled assembly into Definedness.dll
+Rewrote assembly into Definedness.dll
+
+-------------------- FunctionSpecifications --------------------
+Compiled assembly into FunctionSpecifications.dll
+Rewrote assembly into FunctionSpecifications.dll
+
+-------------------- ResolutionErrors --------------------
+ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
+ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)
+ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(261,2): Error: duplicate label
+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+48 resolution/type errors detected in ResolutionErrors.dfy
+
+-------------------- ParseErrors --------------------
+ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
+ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
+ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
+ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
+ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
+8 parse errors detected in ParseErrors.dfy
+
+-------------------- Array --------------------
+Compilation error: Arbitrary type ('B') cannot be compiled
+
+-------------------- MultiDimArray --------------------
+Compiled assembly into MultiDimArray.dll
+Rewrote assembly into MultiDimArray.dll
+
+-------------------- NonGhostQuantifiers --------------------
+NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
+NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+20 resolution/type errors detected in NonGhostQuantifiers.dfy
+
+-------------------- ModulesCycle --------------------
+ModulesCycle.dfy(12,7): Error: module T named among imports does not exist
+ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G
+2 resolution/type errors detected in ModulesCycle.dfy
+
+-------------------- Modules0 --------------------
+Modules0.dfy(5,8): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
+Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
+Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(250,15): Error: unresolved identifier: X
+Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(294,16): Error: member R does not exist in class B
+Modules0.dfy(294,6): Error: expected method call, found expression
+Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
+30 resolution/type errors detected in Modules0.dfy
+
+-------------------- Comprehensions --------------------
+Compiled assembly into Comprehensions.exe
+Rewrote assembly into Comprehensions.exe
+
+-------------------- ControlStructures --------------------
+Compiled assembly into ControlStructures.dll
+Rewrote assembly into ControlStructures.dll
+
+-------------------- ParallelResolveErrors --------------------
+ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field
+ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement
+ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement
+ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements
+ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement
+ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations
+15 resolution/type errors detected in ParallelResolveErrors.dfy
+
+-------------------- Coinductive --------------------
+Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+4 resolution/type errors detected in Coinductive.dfy
+
+-------------------- Corecursion --------------------
+Compiled assembly into Corecursion.dll
+Rewrote assembly into Corecursion.dll
+
+-------------------- LoopModifies --------------------
+Compiled assembly into LoopModifies.dll
+Rewrote assembly into LoopModifies.dll
+
+-------------------- Refinement --------------------
+Compilation error: Method BodyFree._default.M has no body
+
+-------------------- RefinementErrors --------------------
+RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions
+RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause
+RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate
+RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base
+RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F
+RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')
+RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')
+RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')
+RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')
+RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines
+RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G
+11 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- ReturnErrors --------------------
+ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
+ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.
+3 resolution/type errors detected in ReturnErrors.dfy
+
+-------------------- ChainingDisjointTests --------------------
+Compiled assembly into ChainingDisjointTests.dll
+Rewrote assembly into ChainingDisjointTests.dll
+
+-------------------- CallStmtTests --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
+
+-------------------- PredExpr --------------------
+Compiled assembly into PredExpr.dll
+Rewrote assembly into PredExpr.dll
+
+-------------------- Skeletons --------------------
+Compiled assembly into Skeletons.dll
+Rewrote assembly into Skeletons.dll
+
+-------------------- Compilation --------------------
+Compiled assembly into Compilation.exe
+Rewrote assembly into Compilation.exe
diff --git a/Test/dafny0/runtestNoRuntimeChecking.bat b/Test/dafny0/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..c90930d5 --- /dev/null +++ b/Test/dafny0/runtestNoRuntimeChecking.bat @@ -0,0 +1,44 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM Modules1
+REM Termination
+REM Datatypes
+REM NoTypeArgs
+REM ReturnTests
+REM Predicates
+
+for %%f in (Simple TypeTests NatTypes SmallTests Definedness
+ FunctionSpecifications ResolutionErrors ParseErrors
+ Array MultiDimArray NonGhostQuantifiers AdvancedLHS
+ ModulesCycle Modules0 BadFunction Comprehensions
+ Basics ControlStructures DTypes ParallelResolveErrors
+ Parallel TypeParameters Coinductive Corecursion
+ TypeAntecedents SplitExpr LoopModifies Refinement
+ RefinementErrors ReturnErrors ChainingDisjointTests
+ CallStmtTests MultiSets PredExpr LetExpr Skeletons
+ Maps Compilation) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny0/runtestRuntimeChecking.bat b/Test/dafny0/runtestRuntimeChecking.bat new file mode 100644 index 00000000..42d21010 --- /dev/null +++ b/Test/dafny0/runtestRuntimeChecking.bat @@ -0,0 +1,55 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM Modules1
+REM Termination
+REM Datatypes
+REM NoTypeArgs
+REM ReturnTests
+REM Predicates
+
+REM to implement:
+REM SmallTests : unexpected expressions
+REM AdvancedLHS : fresh expressions
+REM BadFunction : ghost state
+REM Basics : ghost state
+REM DTypes : quantifiers
+REM Parallel : quantifiers
+REM TypeParameters : ghost state
+REM TypeAntecedents: quantifiers
+REM SplitExpr : ghost state
+REM MultiSets : quantifiers
+REM LetExpr : old expressions
+REM Maps : quantifiers
+
+for %%f in (Simple TypeTests NatTypes Definedness
+ FunctionSpecifications ResolutionErrors ParseErrors
+ Array MultiDimArray NonGhostQuantifiers ModulesCycle
+ Modules0 Comprehensions ControlStructures ParallelResolveErrors
+ Coinductive Corecursion LoopModifies Refinement
+ RefinementErrors ReturnErrors ChainingDisjointTests
+ CallStmtTests PredExpr Skeletons Compilation) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking new file mode 100644 index 00000000..5472ec14 --- /dev/null +++ b/Test/dafny1/AnswerNoRuntimeChecking @@ -0,0 +1,76 @@ +
+-------------------- Queue --------------------
+Compiled assembly into Queue.dll
+
+-------------------- PriorityQueue --------------------
+Compiled assembly into PriorityQueue.dll
+
+-------------------- ExtensibleArray --------------------
+Compiled assembly into ExtensibleArray.exe
+
+-------------------- ExtensibleArrayAuto --------------------
+Compiled assembly into ExtensibleArrayAuto.exe
+
+-------------------- BinaryTree --------------------
+Compiled assembly into BinaryTree.dll
+
+-------------------- UnboundedStack --------------------
+Compiled assembly into UnboundedStack.dll
+
+-------------------- ListCopy --------------------
+Compilation error: an assume statement cannot be compiled (line 14)
+Compilation error: an assume statement cannot be compiled (line 15)
+
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+
+-------------------- ListContents --------------------
+Compiled assembly into ListContents.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+
+-------------------- SchorrWaite --------------------
+Compiled assembly into SchorrWaite.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+
+-------------------- SumOfCubes --------------------
+Compiled assembly into SumOfCubes.dll
+
+-------------------- FindZero --------------------
+Compiled assembly into FindZero.dll
+
+-------------------- TerminationDemos --------------------
+Compiled assembly into TerminationDemos.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compilation error: an assume statement cannot be compiled (line 66)
+
+-------------------- Induction --------------------
+Compiled assembly into Induction.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
+
+-------------------- Celebrity --------------------
+Compilation error: Function _default._default.Knows has no body
+Compilation error: an assume statement cannot be compiled (line 16)
+
+-------------------- BDD --------------------
+Compiled assembly into BDD.dll
+
+-------------------- UltraFilter --------------------
+Compilation error: Method _default.UltraFilter.H has no body
+Compilation error: an assume statement cannot be compiled (line 42)
+Compilation error: an assume statement cannot be compiled (line 45)
+Compilation error: an assume statement cannot be compiled (line 76)
+Compilation error: an assume statement cannot be compiled (line 97)
+Compilation error: an assume statement cannot be compiled (line 98)
diff --git a/Test/dafny1/AnswerRuntimeChecking b/Test/dafny1/AnswerRuntimeChecking new file mode 100644 index 00000000..1ade5aeb --- /dev/null +++ b/Test/dafny1/AnswerRuntimeChecking @@ -0,0 +1,27 @@ +
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+Rewrote assembly into ListReverse.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+Rewrote assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+Rewrote assembly into pow2.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+Rewrote assembly into Cubes.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+Rewrote assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compiled assembly into KatzManna.dll
+Rewrote assembly into KatzManna.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
diff --git a/Test/dafny1/runtestNoRuntimeChecking.bat b/Test/dafny1/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..a4989fa1 --- /dev/null +++ b/Test/dafny1/runtestNoRuntimeChecking.bat @@ -0,0 +1,36 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM SeparationLogicList
+REM TreeDatatype
+REM MoreInduction
+
+for %%f in (Queue PriorityQueue ExtensibleArray ExtensibleArrayAuto
+ BinaryTree UnboundedStack ListCopy ListReverse ListContents
+ MatrixFun pow2 SchorrWaite Cubes SumOfCubes FindZero
+ TerminationDemos Substitution KatzManna Induction Rippling
+ Celebrity BDD UltraFilter) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny1/runtestRuntimeChecking.bat b/Test/dafny1/runtestRuntimeChecking.bat new file mode 100644 index 00000000..fc32fbf4 --- /dev/null +++ b/Test/dafny1/runtestRuntimeChecking.bat @@ -0,0 +1,51 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM SeparationLogicList
+REM TreeDatatype
+REM MoreInduction
+
+REM to implement:
+REM Queue : parallel statements
+REM PriorityQueue : ghost state
+REM ExtensibleArray : ghost state
+REM ExtensibleArrayAuto: ghost state
+REM BinaryTree : old expressions
+REM UnboundedStack : ghost state
+REM ListCopy : fresh expressions
+REM ListContents : old expressions
+REM SchorrWaite : ghost state
+REM SumOfCubes : ghost state
+REM FindZero : ghost state
+REM TerminationDemos : ghost state
+REM Induction : quantifiers
+REM Celebrity : quantifiers
+REM BDD : ghost state
+REM UltraFilter : quantifiers
+
+for %%f in (ListReverse MatrixFun pow2 Cubes Substitution KatzManna
+ Rippling) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny2/AnswerNoRuntimeChecking b/Test/dafny2/AnswerNoRuntimeChecking new file mode 100644 index 00000000..f04bb934 --- /dev/null +++ b/Test/dafny2/AnswerNoRuntimeChecking @@ -0,0 +1,30 @@ +
+-------------------- Classics --------------------
+Compiled assembly into Classics.dll
+
+-------------------- TreeBarrier --------------------
+Compilation error: an assume statement cannot be compiled (line 90)
+Compilation error: an assume statement cannot be compiled (line 102)
+Compilation error: an assume statement cannot be compiled (line 128)
+
+-------------------- COST-verif-comp-2011-1-MaxArray --------------------
+Compiled assembly into COST-verif-comp-2011-1-MaxArray.dll
+
+-------------------- COST-verif-comp-2011-2-MaxTree-class --------------------
+Compiled assembly into COST-verif-comp-2011-2-MaxTree-class.dll
+
+-------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------
+Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll
+
+-------------------- COST-verif-comp-2011-3-TwoDuplicates --------------------
+Compiled assembly into COST-verif-comp-2011-3-TwoDuplicates.dll
+
+-------------------- COST-verif-comp-2011-4-FloydCycleDetect --------------------
+Compiled assembly into COST-verif-comp-2011-4-FloydCycleDetect.dll
+
+-------------------- Intervals --------------------
+Compiled assembly into Intervals.dll
+
+-------------------- StoreAndRetrieve --------------------
+Compilation error: an assume statement cannot be compiled (line 21)
+Compilation error: Function Library.Function.Apply has no body
diff --git a/Test/dafny2/AnswerRuntimeChecking b/Test/dafny2/AnswerRuntimeChecking new file mode 100644 index 00000000..32b61bb1 --- /dev/null +++ b/Test/dafny2/AnswerRuntimeChecking @@ -0,0 +1,7 @@ +
+-------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------
+Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll
+Rewrote assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll
+
+-------------------- StoreAndRetrieve --------------------
+Compilation error: Function Library.Function.Apply has no body
diff --git a/Test/dafny2/runtestNoRuntimeChecking.bat b/Test/dafny2/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..b60fd69c --- /dev/null +++ b/Test/dafny2/runtestNoRuntimeChecking.bat @@ -0,0 +1,34 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM soon again: SnapshotableTrees.dfy
+
+for %%f in (Classics TreeBarrier COST-verif-comp-2011-1-MaxArray
+ COST-verif-comp-2011-2-MaxTree-class
+ COST-verif-comp-2011-2-MaxTree-datatype
+ COST-verif-comp-2011-3-TwoDuplicates
+ COST-verif-comp-2011-4-FloydCycleDetect
+ Intervals StoreAndRetrieve) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/dafny2/runtestRuntimeChecking.bat b/Test/dafny2/runtestRuntimeChecking.bat new file mode 100644 index 00000000..4ba447a7 --- /dev/null +++ b/Test/dafny2/runtestRuntimeChecking.bat @@ -0,0 +1,39 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM soon again: SnapshotableTrees.dfy
+
+REM to implement:
+REM Classics : ghost state
+REM TreeBarrier : ghost state
+REM COST-verif-comp-2011-1-MaxArray : ghost state
+REM COST-verif-comp-2011-2-MaxTree-class : ghost state
+REM COST-verif-comp-2011-3-TwoDuplicates : quantifiers
+REM COST-verif-comp-2011-4-FloydCycleDetect: quantifiers
+REM Intervals : ghost state
+
+for %%f in (COST-verif-comp-2011-2-MaxTree-datatype
+ StoreAndRetrieve) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vacid0/AnswerNoRuntimeChecking b/Test/vacid0/AnswerNoRuntimeChecking new file mode 100644 index 00000000..a1f7f57b --- /dev/null +++ b/Test/vacid0/AnswerNoRuntimeChecking @@ -0,0 +1,9 @@ +
+-------------------- LazyInitArray --------------------
+Compiled assembly into LazyInitArray.dll
+
+-------------------- SparseArray --------------------
+Compiled assembly into SparseArray.dll
+
+-------------------- Composite --------------------
+Compiled assembly into Composite.exe
diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/Test/vacid0/AnswerRuntimeChecking diff --git a/Test/vacid0/runtestNoRuntimeChecking.bat b/Test/vacid0/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..3a7befa2 --- /dev/null +++ b/Test/vacid0/runtestNoRuntimeChecking.bat @@ -0,0 +1,27 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (LazyInitArray SparseArray Composite) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vacid0/runtestRuntimeChecking.bat b/Test/vacid0/runtestRuntimeChecking.bat new file mode 100644 index 00000000..077c1002 --- /dev/null +++ b/Test/vacid0/runtestRuntimeChecking.bat @@ -0,0 +1,32 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM LazyInitArray: ghost state
+REM SparseArray : ghost state
+REM Composite : ghost state
+
+for %%f in () do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vstte2012/AnswerNoRuntimeChecking b/Test/vstte2012/AnswerNoRuntimeChecking new file mode 100644 index 00000000..c5508749 --- /dev/null +++ b/Test/vstte2012/AnswerNoRuntimeChecking @@ -0,0 +1,18 @@ +
+-------------------- Two-Way-Sort --------------------
+Compiled assembly into Two-Way-Sort.dll
+
+-------------------- Combinators --------------------
+Compiled assembly into Combinators.dll
+
+-------------------- RingBuffer --------------------
+Compiled assembly into RingBuffer.dll
+
+-------------------- RingBufferAuto --------------------
+Compiled assembly into RingBufferAuto.dll
+
+-------------------- Tree --------------------
+Compiled assembly into Tree.dll
+
+-------------------- BreadthFirstSearch --------------------
+Compilation error: Function _default.BreadthFirstSearch.Succ has no body
diff --git a/Test/vstte2012/AnswerRuntimeChecking b/Test/vstte2012/AnswerRuntimeChecking new file mode 100644 index 00000000..5c703cc7 --- /dev/null +++ b/Test/vstte2012/AnswerRuntimeChecking @@ -0,0 +1,11 @@ +
+-------------------- Two-Way-Sort --------------------
+Compiled assembly into Two-Way-Sort.dll
+Rewrote assembly into Two-Way-Sort.dll
+
+-------------------- Tree --------------------
+Compiled assembly into Tree.dll
+Rewrote assembly into Tree.dll
+
+-------------------- BreadthFirstSearch --------------------
+Compilation error: Function _default.BreadthFirstSearch.Succ has no body
diff --git a/Test/vstte2012/runtestNoRuntimeChecking.bat b/Test/vstte2012/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..e572ed2f --- /dev/null +++ b/Test/vstte2012/runtestNoRuntimeChecking.bat @@ -0,0 +1,28 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (Two-Way-Sort Combinators RingBuffer RingBufferAuto
+ Tree BreadthFirstSearch) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
diff --git a/Test/vstte2012/runtestRuntimeChecking.bat b/Test/vstte2012/runtestRuntimeChecking.bat new file mode 100644 index 00000000..042efe96 --- /dev/null +++ b/Test/vstte2012/runtestRuntimeChecking.bat @@ -0,0 +1,32 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM Combinators : ghost state
+REM RingBuffer : ghost state
+REM RingBufferAuto: ghost state
+
+for %%f in (Two-Way-Sort Tree BreadthFirstSearch) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ if exist %%f.cs. (
+ del %%f.cs
+ )
+ if exist %%f.exe. (
+ del %%f.exe
+ )
+ if exist %%f.dll. (
+ del %%f.dll
+ )
+ if exist %%f.pdb. (
+ del %%f.pdb
+ )
+ if exist %%f.pdb.original. (
+ del %%f.pdb.original
+ )
+)
|