diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-31 15:11:03 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-31 15:11:03 -0700 |
| commit | 65334f8f33c92a1e37376d6484d60ee45b55ca1d (patch) | |
| tree | 65f482cd715fb565f0a7ff0cb8b3376d593fd2de /Test/server/simple-session.transcript.expect | |
| parent | 594809c6668c26c3b838153ba4a4222ebef3312d (diff) | |
Add tests for the server
Diffstat (limited to 'Test/server/simple-session.transcript.expect')
| -rw-r--r-- | Test/server/simple-session.transcript.expect | 299 |
1 files changed, 299 insertions, 0 deletions
diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect new file mode 100644 index 00000000..89c3351d --- /dev/null +++ b/Test/server/simple-session.transcript.expect @@ -0,0 +1,299 @@ +# Reading from simple-session.transcript
+transcript(3,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +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]] +transcript(5,13): Error: rbrace expected
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +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]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,0): Error: invalid UpdateStmt
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +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]] +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
+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
+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
+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(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
+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
+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(11,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
+transcript(11,0): Error: semi 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
+transcript(11,0): 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
+transcript(10,25): Error: openparen 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
+transcript(10,25): Error: openparen 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
+transcript(10,26): Error: invalid QSep
+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(10,28): Error: invalid QSep
+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(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
+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
+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
+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
+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
+transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(15,14): Error: Duplicate member name: M'
+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(15,14): Error: Duplicate member name: M'
+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(15,14): Error: Duplicate member name: M'
+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(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+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(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+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(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+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
+transcript(15,14): Error: Duplicate member name: M'
+transcript(24,14): Error: Duplicate member name: M'
+transcript(33,14): Error: Duplicate member name: M'
+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
+transcript(24,14): Error: Duplicate member name: M
+transcript(33,14): Error: Duplicate member name: M
+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
+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
+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
+transcript(38,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
+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
+transcript(38,38): Error: semi 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
+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
+transcript(38,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
+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
+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
+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
+transcript(40,2): 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
+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
+transcript(40,2): 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
+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
+transcript(40,2): 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
+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
+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
+transcript(40,9): Error: invalid AssertStmt
+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
+transcript(40,9): Error: invalid AssertStmt
+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
+transcript(40,9): Error: unresolved identifier: fal
+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
+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
+Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] |