diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 16:15:26 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 16:15:26 -0700 |
| commit | 43cbd76e07262d05434e36dff99f8d10eb59a773 (patch) | |
| tree | 7f2a878e755db64d193530fe9e8f78f15b20b100 | |
| parent | 2f5d59592c5930c32039855824cc49983f643641 (diff) | |
Use /tracePO instead of /trace in the server
This removes the need for special treatment of test input (/trace includes
timings in the output, which are not suitable for tests. /tracePO does not)
| -rw-r--r-- | Source/DafnyServer/Server.cs | 5 | ||||
| -rw-r--r-- | Source/DafnyServer/Utilities.cs | 12 | ||||
| -rw-r--r-- | Source/DafnyServer/VerificationTask.cs | 6 | ||||
| -rw-r--r-- | Test/server/minimal.transcript | 8 | ||||
| -rw-r--r-- | Test/server/minimal.transcript.expect | 14 | ||||
| -rw-r--r-- | Test/server/simple-session.transcript.expect | 694 |
6 files changed, 705 insertions, 34 deletions
diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 0a9ce599..e524a9a3 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -11,7 +11,6 @@ using Microsoft.Boogie; namespace Microsoft.Dafny {
class Server {
- private bool trace;
private bool running;
static void Main(string[] args) {
@@ -25,7 +24,6 @@ namespace Microsoft.Dafny { } else if (hasArg && File.Exists(arg)) {
Console.WriteLine("# Reading from {0}", Path.GetFileName(arg));
Console.SetIn(new StreamReader(arg, Encoding.UTF8));
- server.trace = false;
server.Loop();
} else {
server.Loop();
@@ -40,7 +38,6 @@ namespace Microsoft.Dafny { }
public Server() {
- this.trace = true;
this.running = true;
ExecutionEngine.printer = new DafnyConsolePrinter();
SetupConsole();
@@ -86,7 +83,7 @@ namespace Microsoft.Dafny { if (verb == "verify") {
ServerUtils.checkArgs(command, 0);
var payload = ReadPayload();
- VerificationTask.ReadTask(payload).Run(trace);
+ VerificationTask.ReadTask(payload).Run();
} else if (verb == "quit") {
ServerUtils.checkArgs(command, 0);
Exit();
diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 3bc334b3..d6654ac1 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,18 +43,18 @@ namespace Microsoft.Dafny { }
}
- internal static void ApplyArgs(string[] args, bool trace) {
+ internal static void ApplyArgs(string[] args) {
Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());
Dafny.DafnyOptions.O.ProverKillTime = 10;
if (CommandLineOptions.Clo.Parse(args)) {
// Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME
// Dafny.DafnyOptions.O.ModelViewFile = "-";
- DafnyOptions.O.PrintTooltips = true;
- DafnyOptions.O.UnicodeOutput = true;
- DafnyOptions.O.VerifySnapshots = 2;
- DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);
- DafnyOptions.O.Trace = trace;
+ DafnyOptions.O.VerifySnapshots = 2; // Use caching
+ DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME
+ DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout
+ DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs
+ DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification
} else {
throw new ServerException("Invalid command line options");
}
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index dbafc781..a00688b1 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -44,15 +44,15 @@ namespace Microsoft.Dafny { source = "method selftest() { assert true; }"
};
try {
- task.Run(false);
+ task.Run();
Interaction.EOM(Interaction.SUCCESS, null);
} catch (Exception ex) {
Interaction.EOM(Interaction.FAILURE, ex);
}
}
- internal void Run(bool trace = true) {
- ServerUtils.ApplyArgs(args, trace);
+ internal void Run() {
+ ServerUtils.ApplyArgs(args);
new DafnyHelper(filename, ProgramSource).Verify();
}
}
diff --git a/Test/server/minimal.transcript b/Test/server/minimal.transcript new file mode 100644 index 00000000..9625fb00 --- /dev/null +++ b/Test/server/minimal.transcript @@ -0,0 +1,8 @@ +# RUN: %server "%s" > "%t"
+# RUN: %diff "%s.expect" "%t"
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
diff --git a/Test/server/minimal.transcript.expect b/Test/server/minimal.transcript.expect new file mode 100644 index 00000000..bf3f9dfb --- /dev/null +++ b/Test/server/minimal.transcript.expect @@ -0,0 +1,14 @@ +# Reading from minimal.transcript
+
+Verifying CheckWellformed$$_module.__default.A ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+ [2 proof obligations] error
+transcript(3,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect index 89c3351d..91429d8e 100644 --- a/Test/server/simple-session.transcript.expect +++ b/Test/server/simple-session.transcript.expect @@ -1,24 +1,60 @@ # Reading from simple-session.transcript
+
+Verifying CheckWellformed$$_module.__default.A ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+ [2 proof obligations] error
transcript(3,9): Error: assertion violation
Execution trace:
(0,0): anon0
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [2 proof obligations] error
transcript(3,9): Error: assertion violation
Execution trace:
(0,0): anon0
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [2 proof obligations] error
transcript(3,9): Error: assertion violation
Execution trace:
(0,0): anon0
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [2 proof obligations] error
transcript(3,9): Error: assertion violation
Execution trace:
(0,0): anon0
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+ [0 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,13): Error: rbrace expected
@@ -27,22 +63,114 @@ Verification completed successfully! transcript(6,2): Error: rbrace expected
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [0 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [0 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [0 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,0): Error: invalid UpdateStmt
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [0 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,0): Error: ident expected
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [1 proof obligation] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment
@@ -51,21 +179,113 @@ Verification completed successfully! transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
-Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
-Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
-Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
-Verification completed successfully! -[SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [2 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [2 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [2 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [3 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [3 proof obligations] verified
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [3 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
@@ -77,6 +297,20 @@ transcript(6,2): Error: EOF expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [3 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
@@ -112,15 +346,59 @@ transcript(10,27): Error: invalid UnaryExpression Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [1 proof obligation] error
transcript(10,9): Error: assertion violation
Execution trace:
(0,0): anon0
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
@@ -128,9 +406,39 @@ transcript(12,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
@@ -190,18 +498,130 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+ [5 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+ [5 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+ [2 proof obligations] error
transcript(38,9): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -218,6 +638,44 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+ [2 proof obligations] error
transcript(38,9): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -227,12 +685,90 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+ [2 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+ [2 proof obligations] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
@@ -260,6 +796,44 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
@@ -287,12 +861,90 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+
+Verifying CheckWellformed$$_module.__default.A ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.A ...
+Retrieving cached verification result for implementation Impl$$_module.__default.A...
+ [0 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M_k ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M_k ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M_k...
+ [1 proof obligation] verified
+
+Verifying CheckWellformed$$_module.__default.M0 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M0 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M0...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M1 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M1 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M1...
+ [5 proof obligations] verified
+
+Verifying CheckWellformed$$_module.__default.M2 ...
+Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2...
+ [0 proof obligations] verified
+
+Verifying Impl$$_module.__default.M2 ...
+Retrieving cached verification result for implementation Impl$$_module.__default.M2...
+ [1 proof obligation] verified
Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verification completed successfully! |