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)
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 /Test/server
parent: 2f5d59592c5930c32039855824cc49983f643641 (diff)
3 files changed, 695 insertions, 21 deletions
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!
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 /Test/server
parent	2f5d59592c5930c32039855824cc49983f643641 (diff)