diff options
30 files changed, 4 insertions, 1574 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index fa8ea6da..e72c04dd 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -42,7 +42,6 @@ namespace Microsoft.Dafny { string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))
{
- IncludeCodeContracts();
while (true) {
string s = rd.ReadLine();
if (s == null)
@@ -416,7 +415,7 @@ namespace Microsoft.Dafny { }
}
wr.Write(")");
-
+
wr.WriteLine(";");
Indent(ind + 2 * IndentAmount);
wr.WriteLine("}");
@@ -574,8 +573,6 @@ namespace Microsoft.Dafny { WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
wr.WriteLine(")");
Indent(indent); wr.WriteLine("{");
- TrReq(m.Req, indent + IndentAmount);
- TrEns(m.Ens, indent + IndentAmount);
foreach (Formal p in m.Outs) {
if (!p.IsGhost) {
Indent(indent + IndentAmount);
@@ -855,20 +852,12 @@ namespace Microsoft.Dafny { void TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
- if (!DafnyOptions.O.RuntimeChecking && stmt.IsGhost) {
+ if (stmt.IsGhost) {
CheckHasNoAssumes(stmt);
return;
}
- if (stmt is AssumeStmt)
- {
- TrAssumeStmt((AssumeStmt)stmt, indent);
- }
- else if (stmt is AssertStmt)
- {
- TrAssertStmt((AssertStmt)stmt, indent);
- }
- else if (stmt is PrintStmt) {
+ if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
foreach (Attributes.Argument arg in s.Args) {
SpillLetVariableDecls(arg.E, indent);
@@ -2221,107 +2210,5 @@ namespace Microsoft.Dafny { }
twr.Write(")");
}
-
- #region Runtime checking translation
-
- void IncludeCodeContracts()
- {
- if (DafnyOptions.O.RuntimeChecking)
- {
- wr.WriteLine("using System.Diagnostics.Contracts;");
- }
- }
-
- void TrAssumeStmt(AssumeStmt/*!*/ stmt, int indent)
- {
- Contract.Requires(stmt != null);
-
- Contract.Assert(DafnyOptions.O.RuntimeChecking);
- WriteAssumption(ExprToString(stmt.Expr), indent);
- }
-
- void TrAssertStmt(AssertStmt/*!*/ stmt, int indent)
- {
- Contract.Requires(stmt != null);
-
- Contract.Assert(DafnyOptions.O.RuntimeChecking);
- WriteAssertion(ExprToString(stmt.Expr), indent);
- }
-
- void TrReq(List<MaybeFreeExpression/*!*/>/*!*/ req, int indent)
- {
- Contract.Requires(cce.NonNullElements(req));
-
- if (DafnyOptions.O.RuntimeChecking)
- {
- foreach (MaybeFreeExpression e in req)
- {
- if (!e.IsFree)
- {
- Indent(indent);
- wr.Write("Contract.Requires(");
- TrExpr(e.E);
- wr.WriteLine(");");
- }
- }
- }
- }
-
- void TrEns(List<MaybeFreeExpression/*!*/>/*!*/ ens, int indent)
- {
- Contract.Requires(cce.NonNullElements(ens));
-
- if (DafnyOptions.O.RuntimeChecking)
- {
- foreach (MaybeFreeExpression e in ens)
- {
- if (!e.IsFree)
- {
- Indent(indent);
- wr.Write("Contract.Ensures(");
- TrExpr(e.E);
- wr.WriteLine(");");
- }
- }
- }
- }
-
- #endregion
-
- #region Runtime checking helper methods
-
- string/*!*/ ExprToString(Expression/*!*/ expr)
- {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- TextWriter oldWr = wr;
- wr = new StringWriter();
- TrExpr(expr);
- string e = wr.ToString();
- wr = oldWr;
- return e;
- }
-
- void WriteAssumption(string/*!*/ expr, int indent)
- {
- Contract.Requires(expr != null);
-
- Contract.Assert(DafnyOptions.O.RuntimeChecking);
- Indent(indent);
- wr.WriteLine("Contract.Assume(" + expr + ");");
- }
-
- void WriteAssertion(string/*!*/ expr, int indent)
- {
- Contract.Requires(expr != null);
-
- Contract.Assert(DafnyOptions.O.RuntimeChecking);
- Indent(indent);
- wr.WriteLine("Contract.Assert(" + expr + ");");
- }
-
- #endregion
-
}
}
diff --git a/Dafny/DafnyOptions.cs b/Dafny/DafnyOptions.cs index cb126446..34fa0487 100644 --- a/Dafny/DafnyOptions.cs +++ b/Dafny/DafnyOptions.cs @@ -33,8 +33,6 @@ 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) {
var args = ps.args; // convenient synonym
@@ -92,22 +90,6 @@ 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))
- {
- RuntimeChecking = runtimeChecking == 1;
- }
- return true;
-
default:
break;
}
@@ -166,13 +148,6 @@ 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
- compilation for runtime checking
");
base.Usage(); // also print the Boogie options
}
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 2f7175f4..3534dcbf 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -23,7 +23,6 @@ namespace Microsoft.Dafny using VC;
using System.CodeDom.Compiler;
using AI = Microsoft.AbstractInterpretationFramework;
- using Microsoft.Win32; // needed for ccrewrite
public class DafnyDriver
{
@@ -151,7 +150,7 @@ namespace Microsoft.Dafny if (err != null) {
exitValue = ExitValue.DAFNY_ERROR;
ErrorWriteLine(err);
- } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck && DafnyOptions.O.Verification) {
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
Dafny.Translator translator = new Dafny.Translator();
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
if (CommandLineOptions.Clo.PrintFile != null)
@@ -188,14 +187,6 @@ 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;
}
@@ -240,33 +231,10 @@ namespace Microsoft.Dafny }
cp.GenerateInMemory = false;
cp.ReferencedAssemblies.Add("System.Numerics.dll");
- string ccrewriter = findCCRewriter();
- bool ccrewrite = DafnyOptions.O.RuntimeChecking && ccrewriter != null;
- if (ccrewrite)
- {
- cp.CompilerOptions += " /D:CONTRACTS_FULL";
- }
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
if (cr.Errors.Count == 0) {
Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);
- if (ccrewrite)
- {
- Process p = new Process();
- string ccrewriterOpts = "-nologo -callSiteRequires -shortBranches -throwOnFailure";
- p.StartInfo.FileName = "cmd.exe";
- p.StartInfo.Arguments = "/C \"\"" + ccrewriter + "\" " +
- ccrewriterOpts + " \"" + cp.OutputAssembly + "\"\"";
- p.StartInfo.UseShellExecute = false;
- p.StartInfo.RedirectStandardOutput = true;
- p.Start();
- p.WaitForExit();
- Console.WriteLine("Rewrote assembly into {0}", cr.PathToAssembly);
- }
- else if (ccrewriter == null)
- {
- Console.WriteLine("Error: cannot rewrite, because there is no CodeContracts rewriter");
- }
} else {
Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);
foreach (var ce in cr.Errors) {
@@ -819,56 +787,5 @@ namespace Microsoft.Dafny return PipelineOutcome.VerificationCompleted;
}
-
- #region Runtime checking
-
- /********** Find Code Contracts rewriter **********/
- private static string findCCRewriter()
- {
- using (RegistryKey rk = Registry.CurrentUser.OpenSubKey(@"SOFTWARE"))
- {
- foreach (string skN0 in rk.GetSubKeyNames())
- if (skN0 == "Microsoft")
- using (RegistryKey sk0 = rk.OpenSubKey(skN0))
- {
- foreach (string skN1 in sk0.GetSubKeyNames())
- if (skN1 == "VisualStudio")
- using (RegistryKey sk1 = sk0.OpenSubKey(skN1))
- {
- foreach (string skN2 in sk1.GetSubKeyNames())
- using (RegistryKey sk2 = sk1.OpenSubKey(skN2))
- {
- foreach (string skN3 in sk2.GetSubKeyNames())
- if (skN3 == "CodeTools")
- using (RegistryKey sk3 = sk2.OpenSubKey(skN3))
- {
- foreach (string skN4 in sk3.GetSubKeyNames())
- if (skN4 == "CodeContracts")
- using (RegistryKey sk4 = sk3.OpenSubKey(skN4))
- {
- if ((string)sk4.GetValue("DisplayName") ==
- "Microsoft Code Contracts")
- {
- string ccrewriter =
- (string)sk4.GetValue("InstallDir") +
- "Bin\\ccrewrite.exe";
- if (File.Exists(ccrewriter))
- return ccrewriter;
- else
- return null;
- }
- else
- return null;
- }
- }
- }
- }
- }
- return null;
- }
- }
-
- #endregion
-
}
}
diff --git a/Test/VSComp2010/AnswerNoRuntimeChecking b/Test/VSComp2010/AnswerNoRuntimeChecking deleted file mode 100644 index d0492caf..00000000 --- a/Test/VSComp2010/AnswerNoRuntimeChecking +++ /dev/null @@ -1,15 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 858b6370..00000000 --- a/Test/VSComp2010/AnswerRuntimeChecking +++ /dev/null @@ -1,4 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 4efd244a..00000000 --- a/Test/VSComp2010/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,28 +0,0 @@ -@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 deleted file mode 100644 index d3b8a733..00000000 --- a/Test/VSComp2010/runtestRuntimeChecking.bat +++ /dev/null @@ -1,33 +0,0 @@ -@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 deleted file mode 100644 index 81ac67ef..00000000 --- a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking +++ /dev/null @@ -1,32 +0,0 @@ -
--------------------- b1 --------------------
-Compiled assembly into b1.exe
-
--------------------- b2 --------------------
-Compiled assembly into b2.exe
-
--------------------- b3 --------------------
-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 --------------------
-Compiled assembly into b4.dll
-
--------------------- b5 --------------------
-Compiled assembly into b5.dll
-
--------------------- b6 --------------------
-Compiled assembly into b6.exe
-
--------------------- b7 --------------------
-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 --------------------
-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.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking deleted file mode 100644 index 49a440db..00000000 --- a/Test/VSI-Benchmarks/AnswerRuntimeChecking +++ /dev/null @@ -1,21 +0,0 @@ -
--------------------- b1 --------------------
-Compiled assembly into b1.exe
-Rewrote assembly into b1.exe
-
--------------------- b3 --------------------
-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 --------------------
-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 --------------------
-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.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat deleted file mode 100644 index c85b7606..00000000 --- a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,27 +0,0 @@ -@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-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 /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/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat deleted file mode 100644 index 27df70a3..00000000 --- a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat +++ /dev/null @@ -1,33 +0,0 @@ -@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-
-REM to implement:
-REM b2: quantifiers
-REM b4: old expressions
-REM b5: parallel statements
-REM b6: functions
-
-for %%f in (b1 b3 b7 b8) 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/dafny0/AnswerNoRuntimeChecking b/Test/dafny0/AnswerNoRuntimeChecking deleted file mode 100644 index 04ece8ae..00000000 --- a/Test/dafny0/AnswerNoRuntimeChecking +++ /dev/null @@ -1,328 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index e3970b78..00000000 --- a/Test/dafny0/AnswerRuntimeChecking +++ /dev/null @@ -1,272 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index c90930d5..00000000 --- a/Test/dafny0/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,44 +0,0 @@ -@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 deleted file mode 100644 index 42d21010..00000000 --- a/Test/dafny0/runtestRuntimeChecking.bat +++ /dev/null @@ -1,55 +0,0 @@ -@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 deleted file mode 100644 index 5472ec14..00000000 --- a/Test/dafny1/AnswerNoRuntimeChecking +++ /dev/null @@ -1,76 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 1ade5aeb..00000000 --- a/Test/dafny1/AnswerRuntimeChecking +++ /dev/null @@ -1,27 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index a4989fa1..00000000 --- a/Test/dafny1/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,36 +0,0 @@ -@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 deleted file mode 100644 index fc32fbf4..00000000 --- a/Test/dafny1/runtestRuntimeChecking.bat +++ /dev/null @@ -1,51 +0,0 @@ -@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 deleted file mode 100644 index f04bb934..00000000 --- a/Test/dafny2/AnswerNoRuntimeChecking +++ /dev/null @@ -1,30 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 32b61bb1..00000000 --- a/Test/dafny2/AnswerRuntimeChecking +++ /dev/null @@ -1,7 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index b60fd69c..00000000 --- a/Test/dafny2/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,34 +0,0 @@ -@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 deleted file mode 100644 index 4ba447a7..00000000 --- a/Test/dafny2/runtestRuntimeChecking.bat +++ /dev/null @@ -1,39 +0,0 @@ -@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 deleted file mode 100644 index a1f7f57b..00000000 --- a/Test/vacid0/AnswerNoRuntimeChecking +++ /dev/null @@ -1,9 +0,0 @@ -
--------------------- LazyInitArray --------------------
-Compiled assembly into LazyInitArray.dll
-
--------------------- SparseArray --------------------
-Compiled assembly into SparseArray.dll
-
--------------------- Composite --------------------
-Compiled assembly into Composite.exe
diff --git a/Test/vacid0/runtestNoRuntimeChecking.bat b/Test/vacid0/runtestNoRuntimeChecking.bat deleted file mode 100644 index 3a7befa2..00000000 --- a/Test/vacid0/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,27 +0,0 @@ -@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 deleted file mode 100644 index 077c1002..00000000 --- a/Test/vacid0/runtestRuntimeChecking.bat +++ /dev/null @@ -1,32 +0,0 @@ -@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 deleted file mode 100644 index c5508749..00000000 --- a/Test/vstte2012/AnswerNoRuntimeChecking +++ /dev/null @@ -1,18 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index 5c703cc7..00000000 --- a/Test/vstte2012/AnswerRuntimeChecking +++ /dev/null @@ -1,11 +0,0 @@ -
--------------------- 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 deleted file mode 100644 index e572ed2f..00000000 --- a/Test/vstte2012/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,28 +0,0 @@ -@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 deleted file mode 100644 index 042efe96..00000000 --- a/Test/vstte2012/runtestRuntimeChecking.bat +++ /dev/null @@ -1,32 +0,0 @@ -@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
- )
-)
|