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/Utilities.cs | 60 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 Source/DafnyServer/Utilities.cs (limited to 'Source/DafnyServer/Utilities.cs') diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs new file mode 100644 index 00000000..8fb03b05 --- /dev/null +++ b/Source/DafnyServer/Utilities.cs @@ -0,0 +1,60 @@ +using System; +using System.IO; +using System.Text; +using System.Collections.Generic; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using Microsoft.Boogie; + +namespace Microsoft.Dafny { + class Interaction { + internal static string SUCCESS = "SUCCESS"; + internal static string FAILURE = "FAILURE"; + internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]"; + internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]"; + + internal static void EOM(string header, string msg) { + var trailer = (msg == null) ? "" : "\n"; + Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG); + Console.Out.Flush(); + } + + internal static void EOM(string header, Exception ex, string subHeader = "") { + var aggregate = ex as AggregateException; + subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " "; + + if (aggregate == null) { + EOM(header, subHeader + ex.Message); + } else { + EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); + } + } + } + + class ServerException : Exception { + internal ServerException(string message) : base(message) { } + internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } + } + + class ServerUtils { + internal static void checkArgs(string[] command, int expectedLength) { + if (command.Length - 1 != expectedLength) { + throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength); + } + } + + internal static void ApplyArgs(string[] args) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + + if (CommandLineOptions.Clo.Parse(args)) { + // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME + // Dafny.DafnyOptions.O.ModelViewFile = "-"; + Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.VerifySnapshots = 2; + } else { + throw new ServerException("Invalid command line options"); + } + } + } +} -- cgit v1.2.3 From 593cbcd63017c6a5fe4d50dda34a50637824dfd9 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 13 Aug 2015 10:39:04 -0700 Subject: Add a UniqueIdPrefix in the server and bump up the prover kill time --- Source/DafnyServer/DafnyHelper.cs | 2 +- Source/DafnyServer/Utilities.cs | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) (limited to 'Source/DafnyServer/Utilities.cs') diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 10d98677..f32d0e38 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -62,7 +62,7 @@ namespace Microsoft.Dafny { } private bool Translate() { - var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix + var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = fname }; boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? return true; } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 8fb03b05..20fe0578 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -49,9 +49,10 @@ namespace Microsoft.Dafny { if (CommandLineOptions.Clo.Parse(args)) { // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME // Dafny.DafnyOptions.O.ModelViewFile = "-"; - Dafny.DafnyOptions.O.ProverKillTime = 10; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.ProverKillTime = 20; //FIXME: Should this explicitly override user prefs? + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME Dafny.DafnyOptions.O.VerifySnapshots = 2; + Dafny.DafnyOptions.O.Trace = true; } else { throw new ServerException("Invalid command line options"); } -- cgit v1.2.3 From 4b3fc0e7413424e27131dd8dd919423711f097ad Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 08:46:35 -0700 Subject: Use a nice warning symbol in some warning messages This is useful because trigger-related messages can contain quite a bit of information, especially if they include info about multiple split quantifiers. --- Source/Dafny/DafnyOptions.cs | 1 + Source/Dafny/Triggers/QuantifiersCollection.cs | 58 +++++++++++++++----------- Source/DafnyServer/Server.cs | 4 +- Source/DafnyServer/Utilities.cs | 5 ++- 4 files changed, 40 insertions(+), 28 deletions(-) (limited to 'Source/DafnyServer/Utilities.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 66cf639f..245632ad 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -40,6 +40,7 @@ namespace Microsoft.Dafny Bpl.CommandLineOptions.Install(options); } + public bool UnicodeOutput = false; public bool DisallowSoundnessCheating = false; public bool Dafnycc = false; public int Induction = 3; diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 828e0e18..cbc212d2 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -132,55 +132,63 @@ namespace Microsoft.Dafny.Triggers { //FIXME } - private void CommitOne(QuantifierWithTriggers q, object conjunctId) { + private void CommitOne(QuantifierWithTriggers q, bool addHeader) { var errorLevel = ErrorLevel.Info; var msg = new StringBuilder(); - var indent = conjunctId != null ? " " : " "; - var header = conjunctId != null ? String.Format(" For conjunct {0}:{1}", conjunctId, Environment.NewLine) : ""; + var indent = addHeader ? " " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: no_trigger is passed down to Boogie - msg.Append(indent).AppendLine("Not generating triggers for this quantifier."); + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie + msg.AppendFormat(" Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); + // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) + // FIXME typeQuantifier? } else { - foreach (var candidate in q.Candidates) { - q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); + if (addHeader) { + msg.AppendFormat(" For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } - if (q.Candidates.Any()) { - msg.Append(indent).AppendLine("Selected triggers:"); - foreach (var mc in q.Candidates) { - msg.Append(indent).Append(" ").AppendLine(mc.ToString()); - } + foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger + q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); } - if (q.RejectedCandidates.Any()) { - msg.Append(indent).AppendLine("Rejected triggers:"); - foreach (var mc in q.RejectedCandidates) { - msg.Append(indent).Append(" ").AppendLine(mc.ToString()); - } - } + AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent); + AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); #if QUANTIFIER_WARNINGS + string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension if (!q.CandidateTerms.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("No terms found to trigger on."); + msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on."); } else if (!q.Candidates.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("No trigger covering all quantified variables found."); - } else if (!q.CouldSuppressLoops) { + msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found."); + } else if (!q.CouldSuppressLoops && !q.AllowsLoops) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("Suppressing loops would leave this quantifier without triggers."); + msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); } #endif } - + if (msg.Length > 0) { - reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, header + msg.ToString()); + reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray())); + } + } + + private static void AddTriggersToMessage(string header, List triggers, StringBuilder msg, string indent, bool newlines = false) { + if (triggers.Any()) { + msg.Append(indent).Append(header); + if (triggers.Count == 1) { + msg.Append(" "); + } else if (triggers.Count > 1) { + msg.AppendLine().Append(indent).Append(" "); + } + var separator = newlines && triggers.Count > 1 ? Environment.NewLine + indent + " " : ", "; + msg.AppendLine(String.Join(separator, triggers)); } } internal void CommitTriggers() { foreach (var q in quantifiers) { - CommitOne(q, quantifiers.Count > 1 ? q.quantifier : null); + CommitOne(q, quantifiers.Count > 1); } } } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 74cdd8c2..bdfd66b4 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -33,11 +33,13 @@ namespace Microsoft.Dafny { public Server() { this.running = true; Console.CancelKeyPress += this.CancelKeyPress; + Console.InputEncoding = System.Text.Encoding.UTF8; + Console.OutputEncoding = System.Text.Encoding.UTF8; ExecutionEngine.printer = new DafnyConsolePrinter(); } void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { - e.Cancel = true; + // e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine // Cancel the current verification? TerminateProver() ? Or kill entirely? } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 8fb03b05..4b06e9f5 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,14 @@ namespace Microsoft.Dafny { 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 = "-"; - Dafny.DafnyOptions.O.ProverKillTime = 10; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.UnicodeOutput = true; Dafny.DafnyOptions.O.VerifySnapshots = 2; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); } else { throw new ServerException("Invalid command line options"); } -- 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/Utilities.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 8823b0e75fbf0460ddea5e10f9ee61f5fa171b44 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 15:58:20 -0700 Subject: server: always print tooltips --- Source/DafnyServer/Utilities.cs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'Source/DafnyServer/Utilities.cs') diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 5bd6e7d5..3bc334b3 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -50,10 +50,11 @@ namespace Microsoft.Dafny { if (CommandLineOptions.Clo.Parse(args)) { // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME // Dafny.DafnyOptions.O.ModelViewFile = "-"; - Dafny.DafnyOptions.O.UnicodeOutput = true; - Dafny.DafnyOptions.O.VerifySnapshots = 2; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); - Dafny.DafnyOptions.O.Trace = trace; + 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; } else { throw new ServerException("Invalid command line options"); } -- 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/Utilities.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 e676ad0877d31cb73a1a6bb5aae677ac64593fd6 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 19:58:46 -0700 Subject: Cleanup a number of FIXMEs that I had left in the code --- Source/Dafny/DafnyAst.cs | 12 ++++++------ Source/Dafny/Resolver.cs | 6 +++--- Source/Dafny/Triggers/QuantifiersCollection.cs | 8 ++------ Source/Dafny/Triggers/TriggersCollector.cs | 6 ++++-- Source/DafnyServer/DafnyHelper.cs | 2 +- Source/DafnyServer/Server.cs | 9 +-------- Source/DafnyServer/Utilities.cs | 6 ++---- 7 files changed, 19 insertions(+), 30 deletions(-) (limited to 'Source/DafnyServer/Utilities.cs') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 14a354c4..06f6d856 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7769,7 +7769,7 @@ namespace Microsoft.Dafny { } else if (decl is Method) { Visit((Method)decl); } - //FIXME More? + //TODO More? } public void Visit(Method method) { Visit(method.Ens); @@ -7777,7 +7777,7 @@ namespace Microsoft.Dafny { Visit(method.Mod.Expressions); Visit(method.Decreases.Expressions); if (method.Body != null) { Visit(method.Body); } - //FIXME More? + //TODO More? } public void Visit(Function function) { Visit(function.Ens); @@ -7785,7 +7785,7 @@ namespace Microsoft.Dafny { Visit(function.Reads); Visit(function.Decreases.Expressions); if (function.Body != null) { Visit(function.Body); } - //FIXME More? + //TODO More? } protected virtual void VisitOneExpr(Expression expr) { Contract.Requires(expr != null); @@ -7842,7 +7842,7 @@ namespace Microsoft.Dafny { } else if (decl is Method) { Visit((Method)decl, st); } - //FIXME More? + //TODO More? } public void Visit(Method method, State st) { Visit(method.Ens, st); @@ -7850,7 +7850,7 @@ namespace Microsoft.Dafny { Visit(method.Mod.Expressions, st); Visit(method.Decreases.Expressions, st); if (method.Body != null) { Visit(method.Body, st); } - //FIXME More? + //TODO More? } public void Visit(Function function, State st) { Visit(function.Ens, st); @@ -7858,7 +7858,7 @@ namespace Microsoft.Dafny { Visit(function.Reads, st); Visit(function.Decreases.Expressions, st); if (function.Body != null) { Visit(function.Body, st); } - //FIXME More? + //TODO More? } /// /// Visit one expression proper. This method is invoked before it is invoked on the diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2f2b5a54..e5fe7cf8 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -199,7 +199,7 @@ namespace Microsoft.Dafny public void ResolveProgram(Program prog) { Contract.Requires(prog != null); - var origErrorCount = reporter.Count(ErrorLevel.Error); //FIXME (Clement): This is used further below, but not in the >0 comparisons in the next few lines. Is that right? + var origErrorCount = reporter.Count(ErrorLevel.Error); //TODO: This is used further below, but not in the >0 comparisons in the next few lines. Is that right? var bindings = new ModuleBindings(null); var b = BindModuleNames(prog.DefaultModuleDef, bindings); bindings.BindName("_module", prog.DefaultModule, b); @@ -8301,7 +8301,7 @@ namespace Microsoft.Dafny receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass, true); } else { if (!scope.AllowInstance) { - reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context"); //FIXME: Rephrase this + reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context"); //TODO: Rephrase this // nevertheless, set "receiver" to a value so we can continue resolution } receiver = new ImplicitThisExpr(expr.tok); @@ -8604,7 +8604,7 @@ namespace Microsoft.Dafny Dictionary members; if (classMembers.TryGetValue(cd, out members) && members.TryGetValue(expr.SuffixName, out member)) { if (!member.IsStatic) { - reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName); //FIXME Unify with similar error message + reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName); //TODO Unify with similar error messages // nevertheless, continue creating an expression that approximates a correct one } var receiver = new StaticReceiverExpr(expr.tok, (UserDefinedType)ty.NormalizeExpand(), (ClassDecl)member.EnclosingClass, false); diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index bfa90d81..8e4c3261 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -7,8 +7,6 @@ using System.Text; using Microsoft.Boogie; using System.Diagnostics.Contracts; -//FIXME: When scoring, do not consider old(x) to be higher than x. - namespace Microsoft.Dafny.Triggers { class QuantifierWithTriggers { internal QuantifierExpr quantifier; @@ -149,16 +147,14 @@ namespace Microsoft.Dafny.Triggers { var msg = new StringBuilder(); var indent = addHeader ? " " : ""; - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop, split and autotriggers attributes are passed down to Boogie + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); - // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) - // FIXME typeQuantifier? } else { if (addHeader) { msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } - foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger + foreach (var candidate in q.Candidates) { q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 3b2853ed..30f7b9e8 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -249,10 +249,12 @@ namespace Microsoft.Dafny.Triggers { return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); } - // FIXME document that this will contain duplicates + /// + /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms. + /// internal List CollectTriggers(QuantifierExpr quantifier) { Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier - // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions + // NOTE: We could check for existing trigger attributes and return that instead return Annotate(quantifier).PrivateTerms; } diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 952f71c5..3204fdb3 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -74,7 +74,7 @@ namespace Microsoft.Dafny { ExecutionEngine.CoalesceBlocks(boogieProgram); ExecutionEngine.Inline(boogieProgram); - //FIXME Could capture errors instead of printing them (pass a delegate instead of null) + //NOTE: We could capture errors instead of printing them (pass a delegate instead of null) switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { case PipelineOutcome.Done: case PipelineOutcome.VerificationCompleted: diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index e524a9a3..77840007 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -32,9 +32,8 @@ namespace Microsoft.Dafny { private void SetupConsole() { var utf8 = new UTF8Encoding(false, true); + Console.InputEncoding = utf8; Console.OutputEncoding = utf8; - Console.OutputEncoding = utf8; - Console.CancelKeyPress += CancelKeyPress; } public Server() { @@ -43,12 +42,6 @@ namespace Microsoft.Dafny { SetupConsole(); } - void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { - // e.Cancel = true; - // FIXME TerminateProver and RunningProverFromCommandLine - // Cancel the current verification? TerminateProver()? Or kill entirely? - } - bool EndOfPayload(out string line) { line = Console.ReadLine(); return line == null || line == Interaction.CLIENT_EOM_TAG; diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index d6654ac1..59b3abb9 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,11 @@ namespace Microsoft.Dafny { internal static void ApplyArgs(string[] args) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); - Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { - // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME - // Dafny.DafnyOptions.O.ModelViewFile = "-"; DafnyOptions.O.VerifySnapshots = 2; // Use caching - DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME + 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.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification -- 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/Utilities.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 From 6b1085d784e3773ad9ccbae5bd6b158c97095edc Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 22:51:32 -0700 Subject: Align the server's default kill time with the one of the VS extension --- Source/DafnyServer/Utilities.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/DafnyServer/Utilities.cs') diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 5e2c6f96..30d779e7 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,7 +45,7 @@ namespace Microsoft.Dafny { 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 + Dafny.DafnyOptions.O.ProverKillTime = 10; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { DafnyOptions.O.VerifySnapshots = 2; // Use caching -- 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 'Source/DafnyServer/Utilities.cs') 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