From 65334f8f33c92a1e37376d6484d60ee45b55ca1d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 15:11:03 -0700 Subject: Add tests for the server --- Test/server/simple-session.transcript.expect | 299 +++++++++++++++++++++++++++ 1 file changed, 299 insertions(+) create mode 100644 Test/server/simple-session.transcript.expect (limited to 'Test/server/simple-session.transcript.expect') 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]] -- cgit v1.2.3 From 43cbd76e07262d05434e36dff99f8d10eb59a773 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 16:15:26 -0700 Subject: 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) --- Source/DafnyServer/Server.cs | 5 +- Source/DafnyServer/Utilities.cs | 12 +- Source/DafnyServer/VerificationTask.cs | 6 +- Test/server/minimal.transcript | 8 + Test/server/minimal.transcript.expect | 14 + Test/server/simple-session.transcript.expect | 694 ++++++++++++++++++++++++++- 6 files changed, 705 insertions(+), 34 deletions(-) create mode 100644 Test/server/minimal.transcript create mode 100644 Test/server/minimal.transcript.expect (limited to 'Test/server/simple-session.transcript.expect') 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! -- cgit v1.2.3 From 854acf0f7f5aa105500c6d0ee0fcf0d4c918a81e Mon Sep 17 00:00:00 2001 From: qunyanm Date: Sat, 14 Nov 2015 14:50:26 -0800 Subject: Fix issue 94. Allow tuple-based assignment in statement contexts. --- Source/Dafny/Cloner.cs | 4 + Source/Dafny/Compiler.cs | 8 + Source/Dafny/Dafny.atg | 94 ++++-- Source/Dafny/DafnyAst.cs | 22 ++ Source/Dafny/Parser.cs | 459 +++++++++++++++------------ Source/Dafny/Printer.cs | 13 + Source/Dafny/Resolver.cs | 49 ++- Source/Dafny/Translator.cs | 29 +- Test/dafny4/Bug94.dfy | 35 ++ Test/dafny4/Bug94.dfy.expect | 6 + Test/server/simple-session.transcript.expect | 2 +- 11 files changed, 476 insertions(+), 245 deletions(-) create mode 100644 Test/dafny4/Bug94.dfy create mode 100644 Test/dafny4/Bug94.dfy.expect (limited to 'Test/server/simple-session.transcript.expect') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 1c4275c5..1a6dfecb 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -583,6 +583,10 @@ namespace Microsoft.Dafny var lhss = s.Locals.ConvertAll(c => new LocalVariable(Tok(c.Tok), Tok(c.EndTok), c.Name, CloneType(c.OptionalType), c.IsGhost)); r = new VarDeclStmt(Tok(s.Tok), Tok(s.EndTok), lhss, (ConcreteUpdateStatement)CloneStmt(s.Update)); + } else if (stmt is LetStmt) { + var s = (LetStmt) stmt; + r = new LetStmt(Tok(s.Tok), Tok(s.EndTok), s.LHSs.ConvertAll(CloneCasePattern), s.RHSs.ConvertAll(CloneExpr)); + } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; var mod = CloneSpecFrameExpr(s.Mod); diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 2786133e..82795480 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1764,6 +1764,14 @@ namespace Microsoft.Dafny { wr.Write(TrStmt(s.Update, indent).ToString()); } + } else if (stmt is LetStmt) { + var s = (LetStmt)stmt; + for (int i = 0; i < s.LHSs.Count; i++) { + var lhs = s.LHSs[i]; + if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) { + TrCasePatternOpt(lhs, s.RHSs[i], null, indent, wr, false); + } + } } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; if (s.Body != null) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index ff3b75a3..08c22db4 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1628,46 +1628,74 @@ VarDeclStatement<.out Statement/*!*/ s.> Expression suchThat = null; Attributes attrs = null; IToken endTok; + s = dummyStmt; .) [ "ghost" (. isGhost = true; x = t; .) ] "var" (. if (!isGhost) { x = t; } .) - { Attribute } - LocalIdentTypeOptional (. lhss.Add(d); d.Attributes = attrs; attrs = null; .) - { "," - { Attribute } - LocalIdentTypeOptional (. lhss.Add(d); d.Attributes = attrs; attrs = null; .) - } - [ ":=" (. assignTok = t; .) - Rhs (. rhss.Add(r); .) - { "," Rhs (. rhss.Add(r); .) + ( { Attribute } + LocalIdentTypeOptional (. lhss.Add(d); d.Attributes = attrs; attrs = null; .) + { "," + { Attribute } + LocalIdentTypeOptional (. lhss.Add(d); d.Attributes = attrs; attrs = null; .) } - | { Attribute } - ":|" (. assignTok = t; .) - [ IF(la.kind == _assume) /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */ - "assume" (. suchThatAssume = t; .) + [ ":=" (. assignTok = t; .) + Rhs (. rhss.Add(r); .) + { "," Rhs (. rhss.Add(r); .) + } + | { Attribute } + ":|" (. assignTok = t; .) + [ IF(la.kind == _assume) /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */ + "assume" (. suchThatAssume = t; .) + ] + Expression ] - Expression - ] - SYNC ";" (. endTok = t; .) - (. ConcreteUpdateStatement update; - if (suchThat != null) { - var ies = new List(); - foreach (var lhs in lhss) { - ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name)); - } - update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume, attrs); - } else if (rhss.Count == 0) { - update = null; - } else { - var ies = new List(); - foreach (var lhs in lhss) { - ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name)); + SYNC ";" (. endTok = t; .) + (. ConcreteUpdateStatement update; + if (suchThat != null) { + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume, attrs); + } else if (rhss.Count == 0) { + update = null; + } else { + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new UpdateStmt(assignTok, endTok, ies, rhss); } - update = new UpdateStmt(assignTok, endTok, ies, rhss); - } - s = new VarDeclStmt(x, endTok, lhss, update); - .) + s = new VarDeclStmt(x, endTok, lhss, update); + .) + | "(" (. var letLHSs = new List(); + var letRHSs = new List(); + List arguments = new List(); + CasePattern pat; + Expression e = dummyExpr; + IToken id = t; + .) + [ CasePattern (. arguments.Add(pat); .) + { "," CasePattern (. arguments.Add(pat); .) + } + ] + ")" (. // Parse parenthesis without an identifier as a built in tuple type. + theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists + string ctor = BuiltIns.TupleTypeCtorName; //use the TupleTypeCtors + pat = new CasePattern(id, ctor, arguments); + if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + letLHSs.Add(pat); + .) + ( ":=" + | { Attribute } + ":|" (. SemErr(pat.tok, "LHS of assign-such-that expression must be variables, not general patterns"); .) + ) + Expression (. letRHSs.Add(e); .) + + ";" + (. s = new LetStmt(e.tok, e.tok, letLHSs, letRHSs); .) + ) . IfStmt = (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x; diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 9ed3b7e0..847617aa 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4084,6 +4084,28 @@ namespace Microsoft.Dafny { } } + public class LetStmt : Statement + { + public readonly List LHSs; + public readonly List RHSs; + + public LetStmt(IToken tok, IToken endTok, List lhss, List rhss) + : base(tok, endTok) { + LHSs = lhss; + RHSs = rhss; + } + + public IEnumerable BoundVars { + get { + foreach (var lhs in LHSs) { + foreach (var bv in lhs.Vars) { + yield return bv; + } + } + } + } + } + /// /// Common superclass of UpdateStmt and AssignSuchThatStmt. /// diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index b6a59f4e..922aad75 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -2339,6 +2339,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression suchThat = null; Attributes attrs = null; IToken endTok; + s = dummyStmt; if (la.kind == 73) { Get(); @@ -2346,64 +2347,104 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(78); if (!isGhost) { x = t; } - while (la.kind == 46) { - Attribute(ref attrs); - } - LocalIdentTypeOptional(out d, isGhost); - lhss.Add(d); d.Attributes = attrs; attrs = null; - while (la.kind == 22) { - Get(); + if (la.kind == 1 || la.kind == 46) { while (la.kind == 46) { Attribute(ref attrs); } LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); d.Attributes = attrs; attrs = null; - } - if (la.kind == 25 || la.kind == 46 || la.kind == 95) { - if (la.kind == 95) { + while (la.kind == 22) { Get(); - assignTok = t; - Rhs(out r); - rhss.Add(r); - while (la.kind == 22) { + while (la.kind == 46) { + Attribute(ref attrs); + } + LocalIdentTypeOptional(out d, isGhost); + lhss.Add(d); d.Attributes = attrs; attrs = null; + } + if (la.kind == 25 || la.kind == 46 || la.kind == 95) { + if (la.kind == 95) { Get(); + assignTok = t; Rhs(out r); rhss.Add(r); + while (la.kind == 22) { + Get(); + Rhs(out r); + rhss.Add(r); + } + } else { + while (la.kind == 46) { + Attribute(ref attrs); + } + Expect(25); + assignTok = t; + if (la.kind == _assume) { + Expect(31); + suchThatAssume = t; + } + Expression(out suchThat, false, true); } + } + while (!(la.kind == 0 || la.kind == 28)) {SynErr(184); Get();} + Expect(28); + endTok = t; + ConcreteUpdateStatement update; + if (suchThat != null) { + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume, attrs); + } else if (rhss.Count == 0) { + update = null; } else { + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new UpdateStmt(assignTok, endTok, ies, rhss); + } + s = new VarDeclStmt(x, endTok, lhss, update); + + } else if (la.kind == 50) { + Get(); + var letLHSs = new List(); + var letRHSs = new List(); + List arguments = new List(); + CasePattern pat; + Expression e = dummyExpr; + IToken id = t; + + if (la.kind == 1 || la.kind == 50) { + CasePattern(out pat); + arguments.Add(pat); + while (la.kind == 22) { + Get(); + CasePattern(out pat); + arguments.Add(pat); + } + } + Expect(51); + theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists + string ctor = BuiltIns.TupleTypeCtorName; //use the TupleTypeCtors + pat = new CasePattern(id, ctor, arguments); + if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + letLHSs.Add(pat); + + if (la.kind == 95) { + Get(); + } else if (la.kind == 25 || la.kind == 46) { while (la.kind == 46) { Attribute(ref attrs); } Expect(25); - assignTok = t; - if (la.kind == _assume) { - Expect(31); - suchThatAssume = t; - } - Expression(out suchThat, false, true); - } - } - while (!(la.kind == 0 || la.kind == 28)) {SynErr(184); Get();} - Expect(28); - endTok = t; - ConcreteUpdateStatement update; - if (suchThat != null) { - var ies = new List(); - foreach (var lhs in lhss) { - ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name)); - } - update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume, attrs); - } else if (rhss.Count == 0) { - update = null; - } else { - var ies = new List(); - foreach (var lhs in lhss) { - ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name)); - } - update = new UpdateStmt(assignTok, endTok, ies, rhss); - } - s = new VarDeclStmt(x, endTok, lhss, update); - + SemErr(pat.tok, "LHS of assign-such-that expression must be variables, not general patterns"); + } else SynErr(185); + Expression(out e, false, true); + letRHSs.Add(e); + Expect(28); + s = new LetStmt(e.tok, e.tok, letLHSs, letRHSs); + } else SynErr(186); } void IfStmt(out Statement/*!*/ ifStmt) { @@ -2442,7 +2483,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 46) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; endTok = bs.EndTok; - } else SynErr(185); + } else SynErr(187); } if (guardEllipsis != null) { ifStmt = new SkeletonStatement(new IfStmt(x, endTok, isExistentialGuard, guard, thn, els), guardEllipsis, null); @@ -2450,7 +2491,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ifStmt = new IfStmt(x, endTok, isExistentialGuard, guard, thn, els); } - } else SynErr(186); + } else SynErr(188); } void WhileStmt(out Statement stmt) { @@ -2495,7 +2536,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(59); bodyEllipsis = t; endTok = t; isDirtyLoop = false; } else if (StartOf(23)) { - } else SynErr(187); + } else SynErr(189); if (guardEllipsis != null || bodyEllipsis != null) { if (mod != null) { SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops"); @@ -2513,7 +2554,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, endTok, guard, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), body); } - } else SynErr(188); + } else SynErr(190); } void MatchStmt(out Statement/*!*/ s) { @@ -2538,7 +2579,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseStatement(out c); cases.Add(c); } - } else SynErr(189); + } else SynErr(191); s = new MatchStmt(x, t, e, cases, usesOptionalBrace); } @@ -2563,7 +2604,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)"); - } else SynErr(190); + } else SynErr(192); if (la.kind == _openparen) { Expect(50); if (la.kind == 1) { @@ -2574,7 +2615,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == _ident) { QuantifierDomain(out bvars, out attrs, out range); } - } else SynErr(191); + } else SynErr(193); if (bvars == null) { bvars = new List(); } if (range == null) { range = new LiteralExpr(x, true); } @@ -2664,7 +2705,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 32) { CalcStmt(out subCalc); hintEnd = subCalc.EndTok; subhints.Add(subCalc); - } else SynErr(192); + } else SynErr(194); } var h = new BlockStmt(hintStart, hintEnd, subhints); // if the hint is empty, hintStart is the first token of the next line, but it doesn't matter because the block statement is just used as a container hints.Add(h); @@ -2706,14 +2747,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 59) { Get(); ellipsisToken = t; - } else SynErr(193); + } else SynErr(195); if (la.kind == 46) { BlockStmt(out body, out bodyStart, out endTok); } else if (la.kind == 28) { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(194); Get();} + while (!(la.kind == 0 || la.kind == 28)) {SynErr(196); Get();} Get(); endTok = t; - } else SynErr(195); + } else SynErr(197); s = new ModifyStmt(tok, endTok, mod, attrs, body); if (ellipsisToken != null) { s = new SkeletonStatement(s, ellipsisToken, null); @@ -2733,7 +2774,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 90) { Get(); returnTok = t; isYield = true; - } else SynErr(196); + } else SynErr(198); if (StartOf(26)) { Rhs(out r); rhss = new List(); rhss.Add(r); @@ -2831,7 +2872,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(7)) { Expression(out e, false, true); r = new ExprRhs(e); - } else SynErr(197); + } else SynErr(199); while (la.kind == 46) { Attribute(ref attrs); } @@ -2852,7 +2893,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 27 || la.kind == 48 || la.kind == 50) { Suffix(ref e); } - } else SynErr(198); + } else SynErr(200); } void Expressions(List args) { @@ -2866,6 +2907,56 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } + void CasePattern(out CasePattern pat) { + IToken id; List arguments; + BoundVar bv; + pat = null; + + if (IsIdentParen()) { + Ident(out id); + Expect(50); + arguments = new List(); + if (la.kind == 1 || la.kind == 50) { + CasePattern(out pat); + arguments.Add(pat); + while (la.kind == 22) { + Get(); + CasePattern(out pat); + arguments.Add(pat); + } + } + Expect(51); + pat = new CasePattern(id, id.val, arguments); + } else if (la.kind == 50) { + Get(); + id = t; + arguments = new List(); + + if (la.kind == 1 || la.kind == 50) { + CasePattern(out pat); + arguments.Add(pat); + while (la.kind == 22) { + Get(); + CasePattern(out pat); + arguments.Add(pat); + } + } + Expect(51); + theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists + string ctor = BuiltIns.TupleTypeCtorName; //use the TupleTypeCtors + pat = new CasePattern(id, ctor, arguments); + + } else if (la.kind == 1) { + IdentTypeOptional(out bv); + pat = new CasePattern(bv.tok, bv); + + } else SynErr(201); + if (pat == null) { + pat = new CasePattern(t, "_ParseError", new List()); + } + + } + void AlternativeBlock(bool allowExistentialGuards, out List alternatives, out IToken endTok) { alternatives = new List(); IToken x; @@ -2881,7 +2972,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo isExistentialGuard = true; } else if (StartOf(7)) { Expression(out e, true, false); - } else SynErr(199); + } else SynErr(202); Expect(29); body = new List(); while (StartOf(15)) { @@ -2927,7 +3018,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(7)) { Expression(out ee, true, true); e = ee; - } else SynErr(200); + } else SynErr(203); } void LoopSpec(List invariants, List decreases, ref List mod, ref Attributes decAttrs, ref Attributes modAttrs) { @@ -2935,7 +3026,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo bool isFree = false; Attributes attrs = null; if (la.kind == 37 || la.kind == 88) { - while (!(la.kind == 0 || la.kind == 37 || la.kind == 88)) {SynErr(201); Get();} + while (!(la.kind == 0 || la.kind == 37 || la.kind == 88)) {SynErr(204); Get();} if (la.kind == 88) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); @@ -2948,7 +3039,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo invariants.Add(new MaybeFreeExpression(e, isFree, attrs)); OldSemi(); } else if (la.kind == 36) { - while (!(la.kind == 0 || la.kind == 36)) {SynErr(202); Get();} + while (!(la.kind == 0 || la.kind == 36)) {SynErr(205); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); @@ -2956,7 +3047,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, true, true); OldSemi(); } else if (la.kind == 43) { - while (!(la.kind == 0 || la.kind == 43)) {SynErr(203); Get();} + while (!(la.kind == 0 || la.kind == 43)) {SynErr(206); Get();} Get(); mod = mod ?? new List(); while (IsAttribute()) { @@ -2970,7 +3061,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } OldSemi(); - } else SynErr(204); + } else SynErr(207); } void CaseStatement(out MatchCaseStmt/*!*/ c) { @@ -3007,66 +3098,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo arguments.Add(pat); } Expect(51); - } else SynErr(205); + } else SynErr(208); Expect(29); - while (!(StartOf(28))) {SynErr(206); Get();} + while (!(StartOf(28))) {SynErr(209); Get();} while (IsNotEndOfCase()) { Stmt(body); - while (!(StartOf(28))) {SynErr(207); Get();} + while (!(StartOf(28))) {SynErr(210); Get();} } c = new MatchCaseStmt(x, name, arguments, body); } - void CasePattern(out CasePattern pat) { - IToken id; List arguments; - BoundVar bv; - pat = null; - - if (IsIdentParen()) { - Ident(out id); - Expect(50); - arguments = new List(); - if (la.kind == 1 || la.kind == 50) { - CasePattern(out pat); - arguments.Add(pat); - while (la.kind == 22) { - Get(); - CasePattern(out pat); - arguments.Add(pat); - } - } - Expect(51); - pat = new CasePattern(id, id.val, arguments); - } else if (la.kind == 50) { - Get(); - id = t; - arguments = new List(); - - if (la.kind == 1 || la.kind == 50) { - CasePattern(out pat); - arguments.Add(pat); - while (la.kind == 22) { - Get(); - CasePattern(out pat); - arguments.Add(pat); - } - } - Expect(51); - theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists - string ctor = BuiltIns.TupleTypeCtorName; //use the TupleTypeCtors - pat = new CasePattern(id, ctor, arguments); - - } else if (la.kind == 1) { - IdentTypeOptional(out bv); - pat = new CasePattern(bv.tok, bv); - - } else SynErr(208); - if (pat == null) { - pat = new CasePattern(t, "_ParseError", new List()); - } - - } - void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { bvars = new List(); BoundVar/*!*/ bv; @@ -3161,7 +3202,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Exp; break; } - default: SynErr(209); break; + default: SynErr(211); break; } if (k == null) { op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp); @@ -3176,7 +3217,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 112) { Get(); - } else SynErr(210); + } else SynErr(212); } void ImpliesOp() { @@ -3184,7 +3225,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 114) { Get(); - } else SynErr(211); + } else SynErr(213); } void ExpliesOp() { @@ -3192,7 +3233,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 116) { Get(); - } else SynErr(212); + } else SynErr(214); } void AndOp() { @@ -3200,7 +3241,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 118) { Get(); - } else SynErr(213); + } else SynErr(215); } void OrOp() { @@ -3208,7 +3249,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 120) { Get(); - } else SynErr(214); + } else SynErr(216); } void NegOp() { @@ -3216,7 +3257,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 122) { Get(); - } else SynErr(215); + } else SynErr(217); } void Forall() { @@ -3224,7 +3265,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 123) { Get(); - } else SynErr(216); + } else SynErr(218); } void Exists() { @@ -3232,7 +3273,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 125) { Get(); - } else SynErr(217); + } else SynErr(219); } void QSep() { @@ -3240,7 +3281,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 26) { Get(); - } else SynErr(218); + } else SynErr(220); } void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) { @@ -3275,7 +3316,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); } - } else SynErr(219); + } else SynErr(221); } } @@ -3305,7 +3346,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo RelationalExpression(out e1, allowSemi, allowLambda); e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); } - } else SynErr(220); + } else SynErr(222); } } @@ -3523,7 +3564,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(221); break; + default: SynErr(223); break; } } @@ -3545,7 +3586,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 128) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(222); + } else SynErr(224); } void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -3605,7 +3646,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (IsSuffix()) { Suffix(ref e); } - } else SynErr(223); + } else SynErr(225); } void MulOp(out IToken x, out BinaryExpr.Opcode op) { @@ -3619,7 +3660,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 130) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(224); + } else SynErr(226); } void MapDisplayExpr(IToken/*!*/ mapToken, bool finite, out Expression e) { @@ -3673,13 +3714,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 106) { HashCall(id, out openParen, out typeArgs, out args); } else if (StartOf(31)) { - } else SynErr(225); + } else SynErr(227); e = new ExprDotName(id, e, id.val, typeArgs); if (openParen != null) { e = new ApplySuffix(openParen, e, args); } - } else SynErr(226); + } else SynErr(228); } else if (la.kind == 48) { Get(); x = t; @@ -3727,7 +3768,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(227); + } else SynErr(229); } else if (la.kind == 137) { Get(); anyDots = true; @@ -3735,7 +3776,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee, true, true); e1 = ee; } - } else SynErr(228); + } else SynErr(230); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -3779,7 +3820,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(51); e = new ApplySuffix(openParen, e, args); - } else SynErr(229); + } else SynErr(231); } void ISetDisplayExpr(IToken/*!*/ setToken, bool finite, out Expression e) { @@ -3821,7 +3862,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } Expect(51); - } else SynErr(230); + } else SynErr(232); while (la.kind == 44 || la.kind == 45) { if (la.kind == 44) { Get(); @@ -3904,7 +3945,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e, allowSemi, allowLambda); break; } - default: SynErr(231); break; + default: SynErr(233); break; } } @@ -3919,7 +3960,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 106) { HashCall(id, out openParen, out typeArgs, out args); } else if (StartOf(31)) { - } else SynErr(232); + } else SynErr(234); e = new NameSegment(id, id.val, typeArgs); if (openParen != null) { e = new ApplySuffix(openParen, e, args); @@ -3948,7 +3989,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SeqDisplayExpr(x, elements); Expect(49); - } else SynErr(233); + } else SynErr(235); } void MultiSetExpr(out Expression e) { @@ -3972,7 +4013,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, true, true); e = new MultiSetFormingExpr(x, e); Expect(51); - } else SynErr(234); + } else SynErr(236); } void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) { @@ -4068,7 +4109,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda); break; } - default: SynErr(235); break; + default: SynErr(237); break; } } @@ -4097,7 +4138,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero; } - } else SynErr(236); + } else SynErr(238); } void Dec(out Basetypes.BigDec d) { @@ -4141,7 +4182,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 30) { Get(); oneShot = true; - } else SynErr(237); + } else SynErr(239); } void MapLiteralExpressions(out List elements) { @@ -4204,7 +4245,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CaseExpression(out c, allowSemi, allowLambda); cases.Add(c); } - } else SynErr(238); + } else SynErr(240); e = new MatchExpr(x, e, cases, usesOptionalBrace); } @@ -4222,7 +4263,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 124 || la.kind == 125) { Exists(); x = t; - } else SynErr(239); + } else SynErr(241); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body, allowSemi, allowLambda); @@ -4271,7 +4312,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); } else if (la.kind == 32) { CalcStmt(out s); - } else SynErr(240); + } else SynErr(242); } void LetExpr(out Expression e, bool allowSemi, bool allowLambda) { @@ -4315,7 +4356,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } } - } else SynErr(241); + } else SynErr(243); Expression(out e, false, true); letRHSs.Add(e); while (la.kind == 22) { @@ -4375,7 +4416,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo arguments.Add(pat); } Expect(51); - } else SynErr(242); + } else SynErr(244); Expect(29); Expression(out body, allowSemi, allowLambda); c = new MatchCaseExpr(x, name, arguments, body); @@ -4409,7 +4450,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 2) { Get(); id = t; - } else SynErr(243); + } else SynErr(245); Expect(95); Expression(out e, true, true); } @@ -4452,7 +4493,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 44) { Get(); x = t; - } else SynErr(244); + } else SynErr(246); } @@ -4712,66 +4753,68 @@ public class Errors { case 182: s = "invalid UpdateStmt"; break; case 183: s = "invalid UpdateStmt"; break; case 184: s = "this symbol not expected in VarDeclStatement"; break; - case 185: s = "invalid IfStmt"; break; - case 186: s = "invalid IfStmt"; break; - case 187: s = "invalid WhileStmt"; break; - case 188: s = "invalid WhileStmt"; break; - case 189: s = "invalid MatchStmt"; break; - case 190: s = "invalid ForallStmt"; break; - case 191: s = "invalid ForallStmt"; break; - case 192: s = "invalid CalcStmt"; break; - case 193: s = "invalid ModifyStmt"; break; - case 194: s = "this symbol not expected in ModifyStmt"; break; + case 185: s = "invalid VarDeclStatement"; break; + case 186: s = "invalid VarDeclStatement"; break; + case 187: s = "invalid IfStmt"; break; + case 188: s = "invalid IfStmt"; break; + case 189: s = "invalid WhileStmt"; break; + case 190: s = "invalid WhileStmt"; break; + case 191: s = "invalid MatchStmt"; break; + case 192: s = "invalid ForallStmt"; break; + case 193: s = "invalid ForallStmt"; break; + case 194: s = "invalid CalcStmt"; break; case 195: s = "invalid ModifyStmt"; break; - case 196: s = "invalid ReturnStmt"; break; - case 197: s = "invalid Rhs"; break; - case 198: s = "invalid Lhs"; break; - case 199: s = "invalid AlternativeBlock"; break; - case 200: s = "invalid Guard"; break; - case 201: s = "this symbol not expected in LoopSpec"; break; - case 202: s = "this symbol not expected in LoopSpec"; break; - case 203: s = "this symbol not expected in LoopSpec"; break; - case 204: s = "invalid LoopSpec"; break; - case 205: s = "invalid CaseStatement"; break; - case 206: s = "this symbol not expected in CaseStatement"; break; - case 207: s = "this symbol not expected in CaseStatement"; break; - case 208: s = "invalid CasePattern"; break; - case 209: s = "invalid CalcOp"; break; - case 210: s = "invalid EquivOp"; break; - case 211: s = "invalid ImpliesOp"; break; - case 212: s = "invalid ExpliesOp"; break; - case 213: s = "invalid AndOp"; break; - case 214: s = "invalid OrOp"; break; - case 215: s = "invalid NegOp"; break; - case 216: s = "invalid Forall"; break; - case 217: s = "invalid Exists"; break; - case 218: s = "invalid QSep"; break; - case 219: s = "invalid ImpliesExpliesExpression"; break; - case 220: s = "invalid LogicalExpression"; break; - case 221: s = "invalid RelOp"; break; - case 222: s = "invalid AddOp"; break; - case 223: s = "invalid UnaryExpression"; break; - case 224: s = "invalid MulOp"; break; - case 225: s = "invalid Suffix"; break; - case 226: s = "invalid Suffix"; break; + case 196: s = "this symbol not expected in ModifyStmt"; break; + case 197: s = "invalid ModifyStmt"; break; + case 198: s = "invalid ReturnStmt"; break; + case 199: s = "invalid Rhs"; break; + case 200: s = "invalid Lhs"; break; + case 201: s = "invalid CasePattern"; break; + case 202: s = "invalid AlternativeBlock"; break; + case 203: s = "invalid Guard"; break; + case 204: s = "this symbol not expected in LoopSpec"; break; + case 205: s = "this symbol not expected in LoopSpec"; break; + case 206: s = "this symbol not expected in LoopSpec"; break; + case 207: s = "invalid LoopSpec"; break; + case 208: s = "invalid CaseStatement"; break; + case 209: s = "this symbol not expected in CaseStatement"; break; + case 210: s = "this symbol not expected in CaseStatement"; break; + case 211: s = "invalid CalcOp"; break; + case 212: s = "invalid EquivOp"; break; + case 213: s = "invalid ImpliesOp"; break; + case 214: s = "invalid ExpliesOp"; break; + case 215: s = "invalid AndOp"; break; + case 216: s = "invalid OrOp"; break; + case 217: s = "invalid NegOp"; break; + case 218: s = "invalid Forall"; break; + case 219: s = "invalid Exists"; break; + case 220: s = "invalid QSep"; break; + case 221: s = "invalid ImpliesExpliesExpression"; break; + case 222: s = "invalid LogicalExpression"; break; + case 223: s = "invalid RelOp"; break; + case 224: s = "invalid AddOp"; break; + case 225: s = "invalid UnaryExpression"; break; + case 226: s = "invalid MulOp"; break; case 227: s = "invalid Suffix"; break; case 228: s = "invalid Suffix"; break; case 229: s = "invalid Suffix"; break; - case 230: s = "invalid LambdaExpression"; break; - case 231: s = "invalid EndlessExpression"; break; - case 232: s = "invalid NameSegment"; break; - case 233: s = "invalid DisplayExpr"; break; - case 234: s = "invalid MultiSetExpr"; break; - case 235: s = "invalid ConstAtomExpression"; break; - case 236: s = "invalid Nat"; break; - case 237: s = "invalid LambdaArrow"; break; - case 238: s = "invalid MatchExpression"; break; - case 239: s = "invalid QuantifierGuts"; break; - case 240: s = "invalid StmtInExpr"; break; - case 241: s = "invalid LetExpr"; break; - case 242: s = "invalid CaseExpression"; break; - case 243: s = "invalid MemberBindingUpdate"; break; - case 244: s = "invalid DotSuffix"; break; + case 230: s = "invalid Suffix"; break; + case 231: s = "invalid Suffix"; break; + case 232: s = "invalid LambdaExpression"; break; + case 233: s = "invalid EndlessExpression"; break; + case 234: s = "invalid NameSegment"; break; + case 235: s = "invalid DisplayExpr"; break; + case 236: s = "invalid MultiSetExpr"; break; + case 237: s = "invalid ConstAtomExpression"; break; + case 238: s = "invalid Nat"; break; + case 239: s = "invalid LambdaArrow"; break; + case 240: s = "invalid MatchExpression"; break; + case 241: s = "invalid QuantifierGuts"; break; + case 242: s = "invalid StmtInExpr"; break; + case 243: s = "invalid LetExpr"; break; + case 244: s = "invalid CaseExpression"; break; + case 245: s = "invalid MemberBindingUpdate"; break; + case 246: s = "invalid DotSuffix"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 54de4905..145e82e7 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -963,6 +963,19 @@ namespace Microsoft.Dafny { } wr.Write(";"); + } else if (stmt is LetStmt) { + var s = (LetStmt)stmt; + wr.Write("var"); + string sep = ""; + foreach (var lhs in s.LHSs) { + wr.Write(sep); + PrintCasePattern(lhs); + sep = ", "; + } + wr.Write(" := "); + PrintExpressionList(s.RHSs, true); + wr.WriteLine(";"); + } else if (stmt is SkeletonStatement) { var s = (SkeletonStatement)stmt; if (s.S == null) { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 21476ede..315b823a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2221,6 +2221,10 @@ namespace Microsoft.Dafny foreach (var local in s.Locals) { CheckTypeIsDetermined(local.Tok, local.Type, "local variable"); } + } else if (stmt is LetStmt) { + var s = (LetStmt)stmt; + s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); + } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); @@ -2696,6 +2700,7 @@ namespace Microsoft.Dafny if (s.Update != null) { return CheckTailRecursive(s.Update, enclosingMethod, ref tailCall, reportErrors); } + } else if (stmt is LetStmt) { } else { Contract.Assert(false); // unexpected statement type } @@ -2980,6 +2985,11 @@ namespace Microsoft.Dafny foreach (var v in s.Locals) { CheckEqualityTypes_Type(v.Tok, v.Type); } + } else if (stmt is LetStmt) { + var s = (LetStmt)stmt; + foreach (var v in s.BoundVars) { + CheckEqualityTypes_Type(v.Tok, v.Type); + } } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; // don't recurse on the specification parts, which are ghost @@ -3362,6 +3372,15 @@ namespace Microsoft.Dafny Visit(s.Update, mustBeErasable); } + } else if (stmt is LetStmt) { + var s = (LetStmt)stmt; + if (mustBeErasable) { + foreach (var bv in s.BoundVars) { + bv.IsGhost = true; + } + } + s.IsGhost = s.BoundVars.All(v => v.IsGhost); + } else if (stmt is AssignStmt) { var s = (AssignStmt)stmt; var lhs = s.Lhs.Resolved; @@ -5566,7 +5585,30 @@ namespace Microsoft.Dafny } } } - + } else if (stmt is LetStmt) { + LetStmt s = (LetStmt)stmt; + foreach (var rhs in s.RHSs) { + ResolveExpression(rhs, new ResolveOpts(codeContext, true)); + } + if (s.LHSs.Count != s.RHSs.Count) { + reporter.Error(MessageSource.Resolver, stmt, "let statement must have same number of LHSs (found {0}) as RHSs (found {1})", s.LHSs.Count, s.RHSs.Count); + } + var i = 0; + foreach (var lhs in s.LHSs) { + var rhsType = i < s.RHSs.Count ? s.RHSs[i].Type : new InferredTypeProxy(); + ResolveCasePattern(lhs, rhsType, codeContext); + // Check for duplicate names now, because not until after resolving the case pattern do we know if identifiers inside it refer to bound variables or nullary constructors + var c = 0; + foreach (var bv in lhs.Vars) { + ScopePushAndReport(scope, bv, "local_variable"); + c++; + } + if (c == 0) { + // Every identifier-looking thing in the pattern resolved to a constructor; that is, this LHS is a constant literal + reporter.Error(MessageSource.Resolver, lhs.tok, "LHS is a constant literal; to be legal, it must introduce at least one bound variable"); + } + i++; + } } else if (stmt is AssignStmt) { AssignStmt s = (AssignStmt)stmt; int prevErrorCount = reporter.Count(ErrorLevel.Error); @@ -6748,6 +6790,8 @@ namespace Microsoft.Dafny if (s.Update != null) { CheckForallStatementBodyRestrictions(s.Update, kind); } + } else if (stmt is LetStmt) { + // Are we fine? } else if (stmt is AssignStmt) { var s = (AssignStmt)stmt; CheckForallStatementBodyLhs(s.Tok, s.Lhs.Resolved, kind); @@ -6903,6 +6947,8 @@ namespace Microsoft.Dafny if (s.Update != null) { CheckHintRestrictions(s.Update, localsAllowedInUpdates); } + } else if (stmt is LetStmt) { + // Are we fine? } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; var newScopeForLocals = new HashSet(localsAllowedInUpdates); @@ -7948,7 +7994,6 @@ namespace Microsoft.Dafny ResolveAttributes(e.Attributes, opts); scope.PopMarker(); expr.Type = e.Body.Type; - } else if (expr is NamedExpr) { var e = (NamedExpr)expr; ResolveExpression(e.Body, opts); diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 47dfb96a..51b800a7 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5214,6 +5214,7 @@ namespace Microsoft.Dafny { } CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran); result = null; + } else { // CheckWellformed(var b :| RHS(b); Body(b)) = // var b where typeAntecedent; @@ -7549,7 +7550,32 @@ namespace Microsoft.Dafny { if (s.Update != null) { TrStmt(s.Update, builder, locals, etran); } - + } else if (stmt is LetStmt) { + var s = (LetStmt)stmt; + foreach (var bv in s.BoundVars) { + Bpl.LocalVariable bvar = new Bpl.LocalVariable(bv.Tok, new Bpl.TypedIdent(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), TrType(bv.Type))); + locals.Add(bvar); + var bIe = new Bpl.IdentifierExpr(bvar.tok, bvar); + builder.Add(new Bpl.HavocCmd(bv.Tok, new List { bIe })); + Bpl.Expr wh = GetWhereClause(bv.Tok, bIe, bv.Type, etran); + if (wh != null) { + builder.Add(new Bpl.AssumeCmd(bv.Tok, wh)); + } + } + Contract.Assert(s.LHSs.Count == s.RHSs.Count); // checked by resolution + var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("let#"); + for (int i = 0; i < s.LHSs.Count; i++) { + var pat = s.LHSs[i]; + var rhs = s.RHSs[i]; + var nm = varNameGen.FreshId(string.Format("#{0}#", i)); + var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type))); + locals.Add(r); + var rIe = new Bpl.IdentifierExpr(pat.tok, r); + TrStmt_CheckWellformed(s.RHSs[i], builder, locals, etran, false); + CheckWellformedWithResult(s.RHSs[i], new WFOptions(null, false, false), rIe, pat.Expr.Type, locals, builder, etran); + CheckCasePatternShape(pat, rIe, builder); + builder.Add(new Bpl.AssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(pat.Expr), rIe))); + } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } @@ -13700,6 +13726,7 @@ namespace Microsoft.Dafny { if (newCasePatterns != e.LHSs) { anythingChanged = true; } + var body = Substitute(e.Body); // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.Vars) foreach (var bv in e.BoundVars) { diff --git a/Test/dafny4/Bug94.dfy b/Test/dafny4/Bug94.dfy new file mode 100644 index 00000000..2f437785 --- /dev/null +++ b/Test/dafny4/Bug94.dfy @@ -0,0 +1,35 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function foo() : (int, int) +{ + (5, 10) +} + +function bar() : int +{ + var (x, y) := foo(); + x + y +} + +lemma test() +{ + var (x, y) := foo(); +} + +function method foo2() : (int,int) +{ + (5, 10) +} + +method test2() +{ + var (x, y) := foo2(); +} + +method Main() +{ + var (x, y) := foo2(); + assert (x+y == 15); + print(x+y); +} diff --git a/Test/dafny4/Bug94.dfy.expect b/Test/dafny4/Bug94.dfy.expect new file mode 100644 index 00000000..6b337d5a --- /dev/null +++ b/Test/dafny4/Bug94.dfy.expect @@ -0,0 +1,6 @@ + +Dafny program verifier finished with 9 verified, 0 errors +Program compiled successfully +Running... + +15 \ No newline at end of file diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect index 91429d8e..1aadca7f 100644 --- a/Test/server/simple-session.transcript.expect +++ b/Test/server/simple-session.transcript.expect @@ -136,7 +136,7 @@ Retrieving cached verification result for implementation Impl$$_module.__default [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -transcript(7,0): Error: ident expected +transcript(7,0): Error: invalid VarDeclStatement Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] -- cgit v1.2.3 From 91cee1c2028f9ad995df863f2a4568d95f4ea1a8 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 28 Mar 2016 12:02:37 -0700 Subject: Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. --- Source/Dafny/DafnyOptions.cs | 6 ++-- Source/DafnyServer/Utilities.cs | 2 +- Test/VSI-Benchmarks/b8.dfy | 2 +- Test/VerifyThis2015/Problem3.dfy | 2 +- Test/cloudmake/CloudMake-CachedBuilds.dfy | 2 +- Test/cloudmake/CloudMake-ConsistentBuilds.dfy | 2 +- Test/cloudmake/CloudMake-ParallelBuilds.dfy | 2 +- Test/dafny0/Basics.dfy | 2 +- Test/dafny0/Calculations.dfy | 2 +- Test/dafny0/Compilation.dfy | 2 +- Test/dafny0/ForallCompilation.dfy | 2 +- Test/dafny0/Fuel.dfy | 2 +- Test/dafny0/LetExpr.dfy | 2 +- Test/dafny0/LetExpr.dfy.expect | 1 + Test/dafny0/LhsDuplicates.dfy | 2 +- Test/dafny0/Parallel.dfy | 2 +- Test/dafny0/SmallTests.dfy.expect | 1 + Test/dafny1/MoreInduction.dfy | 2 +- Test/dafny1/SchorrWaite-stages.dfy | 2 +- Test/dafny1/SchorrWaite.dfy | 2 +- Test/dafny1/Substitution.dfy | 2 +- Test/dafny1/UltraFilter.dfy | 2 +- Test/dafny2/SnapshotableTrees.dfy | 2 +- Test/dafny3/Filter.dfy | 2 +- Test/dafny4/GHC-MergeSort.dfy | 2 +- Test/dafny4/NumberRepresentations.dfy | 2 +- Test/dafny4/Primes.dfy | 2 +- Test/server/simple-session.transcript.expect | 41 +++++++++++++++++++++++++++ Test/vstte2012/BreadthFirstSearch.dfy | 2 +- 29 files changed, 71 insertions(+), 28 deletions(-) (limited to 'Test/server/simple-session.transcript.expect') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index f3b38a84..607090eb 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = true; public bool RewriteFocalPredicates = true; public bool PrintTooltips = false; public bool PrintStats = false; @@ -386,8 +386,8 @@ namespace Microsoft.Dafny 1 (default) - If preprocessing succeeds, set exit code to the number of verification errors. /autoTriggers: - 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. - 1 - Add a {:trigger} to each user-level quantifier. Existing + 0 - Do not generate {:trigger} annotations for user-level quantifiers. + 1 (default) - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. /rewriteFocalPredicates: 0 - Don't rewrite predicates in the body of prefix lemmas. diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 30d779e7..48bea01a 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -51,7 +51,7 @@ namespace Microsoft.Dafny { DafnyOptions.O.VerifySnapshots = 2; // Use caching DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout - DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs + //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/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index ea1911fe..a44ff5c3 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Benchmark 8 diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 21bdd4ed..60506a33 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy index 9e1b511e..5f16da90 100644 --- a/Test/cloudmake/CloudMake-CachedBuilds.dfy +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy index 6d86607b..c2fa4205 100644 --- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy +++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" /******* State *******/ diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index 07cae317..5cc70994 100644 --- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 89b0f02a..7b8b632b 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Global { diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index a7c8e06c..eb4ff1b9 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 7a443e47..213ace54 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %dafny /compile:3 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The tests in this file are designed to run through the compiler. They contain diff --git a/Test/dafny0/ForallCompilation.dfy b/Test/dafny0/ForallCompilation.dfy index c812983a..4d89f70d 100644 --- a/Test/dafny0/ForallCompilation.dfy +++ b/Test/dafny0/ForallCompilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index 6347e134..a768db02 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" module TestModule1 { diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 000fce53..6a0ca66b 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index f0f51274..8f365da3 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -35,5 +35,6 @@ Execution trace: (0,0): anon10_Then Dafny program verifier finished with 39 verified, 9 errors +LetExpr.dfy.tmp.dprint.dfy(162,2): Warning: /!\ No terms found to trigger on. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy index 6a84c5a5..8a57f6ce 100644 --- a/Test/dafny0/LhsDuplicates.dfy +++ b/Test/dafny0/LhsDuplicates.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class MyClass { diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 93a16475..00a1514c 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 6161c3dd..746e978a 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -197,5 +197,6 @@ Execution trace: (0,0): anon0 Dafny program verifier finished with 104 verified, 35 errors +SmallTests.dfy.tmp.dprint.dfy(369,4): Warning: /!\ No trigger covering all quantified variables found. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index bd654db5..2b5187a4 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(Node, List) diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 0eaed68c..a6e5e3aa 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Schorr-Waite algorithms, written and verified in Dafny. diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 50210eb1..b0877f9f 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index da64d004..b9c83aff 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(Expr, List) diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index a32e6e0b..7ac4e749 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // ultra filter diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy index 2bdfb83b..033c5db0 100644 --- a/Test/dafny2/SnapshotableTrees.dfy +++ b/Test/dafny2/SnapshotableTrees.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:2 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:2 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino, September 2011. diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index 4f8b35ec..7473a580 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" codatatype Stream = Cons(head: T, tail: Stream) diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy index 976b8a27..24903d87 100644 --- a/Test/dafny4/GHC-MergeSort.dfy +++ b/Test/dafny4/GHC-MergeSort.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 0d6cffa1..c15f4987 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // We consider a number representation that consists of a sequence of digits. The least diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy index fd64b45e..0c2a64dd 100644 --- a/Test/dafny4/Primes.dfy +++ b/Test/dafny4/Primes.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" predicate IsPrime(n: int) diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect index 1aadca7f..a5f841bc 100644 --- a/Test/server/simple-session.transcript.expect +++ b/Test/server/simple-session.transcript.expect @@ -346,6 +346,7 @@ 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): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -366,6 +367,7 @@ Execution trace: 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): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -383,6 +385,7 @@ Verifying Impl$$_module.__default.M_k ... 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): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -406,6 +409,7 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -423,6 +427,7 @@ Verifying Impl$$_module.__default.M_k ... 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): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -498,6 +503,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -538,6 +547,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -584,6 +597,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -638,6 +655,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -685,6 +706,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -729,6 +754,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -796,6 +825,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -861,6 +894,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -905,6 +942,10 @@ 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 +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index b111a438..375f4a09 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class BreadthFirstSearch -- cgit v1.2.3