From 990966db7dcea00045c5c104ded084348e8f7dde Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 14:26:53 -0700 Subject: Split the server source into multiple files --- Source/DafnyServer/VerificationTask.cs | 59 ++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 Source/DafnyServer/VerificationTask.cs (limited to 'Source/DafnyServer/VerificationTask.cs') diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs new file mode 100644 index 00000000..a00688b1 --- /dev/null +++ b/Source/DafnyServer/VerificationTask.cs @@ -0,0 +1,59 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using System.Text; +using System.Threading.Tasks; + +namespace Microsoft.Dafny { + [Serializable] + class VerificationTask { + [DataMember] + string[] args = null; + + [DataMember] + string filename = null; + + [DataMember] + string source = null; + + [DataMember] + bool sourceIsFile = false; + + string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } + + internal static VerificationTask ReadTask(string b64_repr) { + try { + var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); + using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { + DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); + return (VerificationTask)serializer.ReadObject(ms); + } + } catch (Exception ex) { + throw new ServerException("Deserialization failed: {0}.", ex.Message); + } + } + + internal static void SelfTest() { + var task = new VerificationTask() { + filename = "", + sourceIsFile = false, + args = new string[] { }, + source = "method selftest() { assert true; }" + }; + try { + task.Run(); + Interaction.EOM(Interaction.SUCCESS, null); + } catch (Exception ex) { + Interaction.EOM(Interaction.FAILURE, ex); + } + } + + internal void Run() { + ServerUtils.ApplyArgs(args); + new DafnyHelper(filename, ProgramSource).Verify(); + } + } +} -- cgit v1.2.3 From a019d797bd42866242e48ef00850f74e3bdc9241 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 16:41:10 -0700 Subject: Server: disable tracing when running tests, and fix an encoding issue. z3 doesn't support byte-order marks; thus using the default UTF8Encoding object (to allow printing nice warning signs) causes issues, as it sends a BOM before anything else. --- Source/DafnyServer/Server.cs | 24 ++++++++++++++++-------- Source/DafnyServer/Utilities.cs | 3 ++- Source/DafnyServer/VerificationTask.cs | 6 +++--- 3 files changed, 21 insertions(+), 12 deletions(-) (limited to 'Source/DafnyServer/VerificationTask.cs') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index bdfd66b4..0a9ce599 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -11,6 +11,7 @@ using Microsoft.Boogie; namespace Microsoft.Dafny { class Server { + private bool trace; private bool running; static void Main(string[] args) { @@ -23,33 +24,40 @@ namespace Microsoft.Dafny { VerificationTask.SelfTest(); } else if (hasArg && File.Exists(arg)) { Console.WriteLine("# Reading from {0}", Path.GetFileName(arg)); - Console.SetIn(new StreamReader(arg)); + Console.SetIn(new StreamReader(arg, Encoding.UTF8)); + server.trace = false; server.Loop(); } else { server.Loop(); } } + private void SetupConsole() { + var utf8 = new UTF8Encoding(false, true); + Console.OutputEncoding = utf8; + Console.OutputEncoding = utf8; + Console.CancelKeyPress += CancelKeyPress; + } + public Server() { + this.trace = true; this.running = true; - Console.CancelKeyPress += this.CancelKeyPress; - Console.InputEncoding = System.Text.Encoding.UTF8; - Console.OutputEncoding = System.Text.Encoding.UTF8; ExecutionEngine.printer = new DafnyConsolePrinter(); + SetupConsole(); } void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { // e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine - // Cancel the current verification? TerminateProver() ? Or kill entirely? + // Cancel the current verification? TerminateProver()? Or kill entirely? } - static bool EndOfPayload(out string line) { + bool EndOfPayload(out string line) { line = Console.ReadLine(); return line == null || line == Interaction.CLIENT_EOM_TAG; } - static string ReadPayload() { + string ReadPayload() { StringBuilder buffer = new StringBuilder(); string line = null; while (!EndOfPayload(out line)) { @@ -78,7 +86,7 @@ namespace Microsoft.Dafny { if (verb == "verify") { ServerUtils.checkArgs(command, 0); var payload = ReadPayload(); - VerificationTask.ReadTask(payload).Run(); + VerificationTask.ReadTask(payload).Run(trace); } else if (verb == "quit") { ServerUtils.checkArgs(command, 0); Exit(); diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 4b06e9f5..96254a3d 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,7 +43,7 @@ namespace Microsoft.Dafny { } } - internal static void ApplyArgs(string[] args) { + internal static void ApplyArgs(string[] args, bool trace) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); Dafny.DafnyOptions.O.ProverKillTime = 10; @@ -53,6 +53,7 @@ namespace Microsoft.Dafny { Dafny.DafnyOptions.O.UnicodeOutput = true; Dafny.DafnyOptions.O.VerifySnapshots = 2; Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.Clo.Trace = trace; } else { throw new ServerException("Invalid command line options"); } diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index a00688b1..dbafc781 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(); + task.Run(false); Interaction.EOM(Interaction.SUCCESS, null); } catch (Exception ex) { Interaction.EOM(Interaction.FAILURE, ex); } } - internal void Run() { - ServerUtils.ApplyArgs(args); + internal void Run(bool trace = true) { + ServerUtils.ApplyArgs(args, trace); new DafnyHelper(filename, ProgramSource).Verify(); } } -- 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 'Source/DafnyServer/VerificationTask.cs') 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 8ede9fda35767f083899940886b69f53640891c9 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 18:59:10 -0700 Subject: Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience) Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations). --- Binaries/z3 | Bin 16438468 -> 0 bytes Source/Dafny/DafnyOptions.cs | 37 ++++++++++++++++++++++++++++----- Source/Dafny/Reporting.cs | 2 +- Source/DafnyDriver/DafnyDriver.cs | 14 ++++++------- Source/DafnyServer/DafnyHelper.cs | 5 ++++- Source/DafnyServer/Utilities.cs | 4 ++-- Source/DafnyServer/VerificationTask.cs | 3 +-- 7 files changed, 47 insertions(+), 18 deletions(-) delete mode 100755 Binaries/z3 (limited to 'Source/DafnyServer/VerificationTask.cs') diff --git a/Binaries/z3 b/Binaries/z3 deleted file mode 100755 index 7c60feb4..00000000 Binary files a/Binaries/z3 and /dev/null differ diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 1986ea6d..08e53d5c 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -9,8 +9,11 @@ namespace Microsoft.Dafny { public class DafnyOptions : Bpl.CommandLineOptions { - public DafnyOptions() + private ErrorReporter errorReporter; + + public DafnyOptions(ErrorReporter errorReporter = null) : base("Dafny", "Dafny program verifier") { + this.errorReporter = errorReporter; SetZ3ExecutableName(); } @@ -257,13 +260,37 @@ namespace Microsoft.Dafny // TODO: provide attribute help here } + + /// + /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. + /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script. + /// For developers though (and people getting this from source), it's convenient to be able to run right away, + /// so we vendor a Windows version. + /// private void SetZ3ExecutableName() { var platform = (int)System.Environment.OSVersion.Platform; - var isLinux = platform == 4 || platform == 128; // http://www.mono-project.com/docs/faq/technical/ - //TODO should we also vendor an OSX build? - var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); - Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe"); + // http://www.mono-project.com/docs/faq/technical/ + var isUnix = platform == 4 || platform == 128; + + var z3binName = isUnix ? "z3" : "z3.exe"; + var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); + var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin"); + var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName); + + if (!System.IO.File.Exists(z3BinPath) && !isUnix) { + // This is most likely a Windows user running from source without downloading z3 + // separately; this is ok, since we vendor z3.exe. + z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName); + } + + if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) { + var tok = new Bpl.Token(1, 1) { filename = "*** " }; + errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", + z3binName, z3BinDir, System.Environment.NewLine); + } else { + Z3ExecutablePath = z3BinPath; + } } public override void Usage() { diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 4cfbf20e..760392ca 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -143,7 +143,7 @@ namespace Microsoft.Dafny { } public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { - if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) { + if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) { // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI msg = msg.Replace(Environment.NewLine, Environment.NewLine + " "); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 4b5ae8d8..c45d66fc 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -40,10 +40,11 @@ namespace Microsoft.Dafny public static int ThreadMain(string[] args) { Contract.Requires(cce.NonNullElements(args)); - + + ErrorReporter reporter = new ConsoleErrorReporter(); ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors - DafnyOptions.Install(new DafnyOptions()); + DafnyOptions.Install(new DafnyOptions(reporter)); ExitValue exitValue = ExitValue.VERIFIED; CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; @@ -92,7 +93,7 @@ namespace Microsoft.Dafny goto END; } } - exitValue = ProcessFiles(CommandLineOptions.Clo.Files); + exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter); END: if (CommandLineOptions.Clo.XmlSink != null) { @@ -112,7 +113,7 @@ namespace Microsoft.Dafny } - static ExitValue ProcessFiles(IList/*!*/ fileNames, bool lookForSnapshots = true, string programId = null) + static ExitValue ProcessFiles(IList/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(fileNames)); @@ -128,7 +129,7 @@ namespace Microsoft.Dafny { Console.WriteLine(); Console.WriteLine("-------------------- {0} --------------------", f); - var ev = ProcessFiles(new List { f }, lookForSnapshots, f); + var ev = ProcessFiles(new List { f }, reporter, lookForSnapshots, f); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -142,7 +143,7 @@ namespace Microsoft.Dafny var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames); foreach (var s in snapshotsByVersion) { - var ev = ProcessFiles(new List(s), false, programId); + var ev = ProcessFiles(new List(s), reporter, false, programId); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -153,7 +154,6 @@ namespace Microsoft.Dafny using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) { Dafny.Program dafnyProgram; - ErrorReporter reporter = new ConsoleErrorReporter(); string programName = fileNames.Count == 1 ? fileNames[0] : "the program"; string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram); if (err != null) { diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 3204fdb3..e54e2b48 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -29,18 +29,21 @@ namespace Microsoft.Dafny { class DafnyHelper { private string fname; private string source; + private string[] args; private readonly Dafny.ErrorReporter reporter; private Dafny.Program dafnyProgram; private Bpl.Program boogieProgram; - public DafnyHelper(string fname, string source) { + public DafnyHelper(string[] args, string fname, string source) { + this.args = args; this.fname = fname; this.source = source; this.reporter = new Dafny.ConsoleErrorReporter(); } public bool Verify() { + ServerUtils.ApplyArgs(args, reporter); return Parse() && Resolve() && Translate() && Boogie(); } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 59b3abb9..5e2c6f96 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,8 +43,8 @@ namespace Microsoft.Dafny { } } - internal static void ApplyArgs(string[] args) { - Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + internal static void ApplyArgs(string[] args, ErrorReporter reporter) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter)); Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index a00688b1..eb740e70 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -52,8 +52,7 @@ namespace Microsoft.Dafny { } internal void Run() { - ServerUtils.ApplyArgs(args); - new DafnyHelper(filename, ProgramSource).Verify(); + new DafnyHelper(args, filename, ProgramSource).Verify(); } } } -- cgit v1.2.3