From e93d4804f9d99150079728572c00a518af20a7c5 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 30 Jul 2015 12:04:16 -0700 Subject: Implement a Dafny server. The Dafny server is a command line utility that allows non-.Net editors to take advantage of Dafny's caching facilities, as used by the Dafny extension for Visual Studio. The server is essentially a REPL, which produces output in the same format as the Dafny CLI; clients thus do not need to understand the internals of Dafny's caching. A typical editing session proceeds as follows: * When a new Dafny file is opened, the editor starts a new instance of the Dafny server. The cache is blank at that point. * The editor sends a copy of the buffer for initial verification. This takes some time, after which the server returns a list of errors. * The user makes modifications; the editor periodically sends a new copy of the buffer's contents to the Dafny server, which quickly returns an updated list of errors. The client-server protocol is sequential, uses JSON, and works over ASCII pipes by base64-encoding queries. It defines one type of query, and two types of responses: Queries are of the following form: verify [[DAFNY-CLIENT: EOM]] Responses are of the following form: [SUCCESS] [[DAFNY-SERVER: EOM]] or [FAILURE] [[DAFNY-SERVER: EOM]] The JSON payload is an array with 4 fields: * args: An array of Dafny arguments, as passed to the Dafny CLI * source: A Dafny program, or the path to a Dafny source file. * sourceIsFile: A boolean indicating whether the 'source' argument is a Dafny program or the path to one. * filename: The name of the original source file, to be used in error messages For small files, embedding the Dafny source directly into a message is convenient; for larger files, however, it is generally better for performance to write the source snapshot to a separate file, and to pass that to Dafny by setting the 'sourceIsFile' flag to true. --- Source/DafnyServer/DafnyServer.csproj | 75 +++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 Source/DafnyServer/DafnyServer.csproj (limited to 'Source/DafnyServer/DafnyServer.csproj') diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj new file mode 100644 index 00000000..0aac88b2 --- /dev/null +++ b/Source/DafnyServer/DafnyServer.csproj @@ -0,0 +1,75 @@ + + + + + Debug + AnyCPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2} + Exe + Properties + DafnyServer + DafnyServer + v4.5 + 512 + Microsoft.Dafny.Server + + + true + full + false + ..\..\Binaries\ + DEBUG;TRACE + prompt + 4 + + + AnyCPU + pdbonly + true + ..\..\Binaries\ + TRACE + prompt + 4 + + + + ..\..\..\boogie\Binaries\Core.dll + + + ..\..\..\boogie\Binaries\ExecutionEngine.dll + + + ..\..\..\boogie\Binaries\ParserHelper.dll + + + ..\..\..\boogie\Binaries\Provers.SMTLib.dll + + + + + + + + ..\..\Binaries\DafnyPipeline.dll + + + + + + + + + + + PreserveNewest + + + + + -- cgit v1.2.3 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/DafnyHelper.cs | 87 ++++++++++++++ Source/DafnyServer/DafnyServer.csproj | 7 +- Source/DafnyServer/Server.cs | 202 +++------------------------------ Source/DafnyServer/Utilities.cs | 60 ++++++++++ Source/DafnyServer/VerificationTask.cs | 59 ++++++++++ 5 files changed, 227 insertions(+), 188 deletions(-) create mode 100644 Source/DafnyServer/DafnyHelper.cs create mode 100644 Source/DafnyServer/Utilities.cs create mode 100644 Source/DafnyServer/VerificationTask.cs (limited to 'Source/DafnyServer/DafnyServer.csproj') diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs new file mode 100644 index 00000000..10d98677 --- /dev/null +++ b/Source/DafnyServer/DafnyHelper.cs @@ -0,0 +1,87 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; +using Bpl = Microsoft.Boogie; + +namespace Microsoft.Dafny { + // FIXME: This should not be duplicated here + class DafnyConsolePrinter : ConsolePrinter { + public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { + // Dafny has 0-indexed columns, but Boogie counts from 1 + var realigned_tok = new Token(tok.line, tok.col - 1); + realigned_tok.kind = tok.kind; + realigned_tok.pos = tok.pos; + realigned_tok.val = tok.val; + realigned_tok.filename = tok.filename; + base.ReportBplError(realigned_tok, message, error, tw, category); + + if (tok is Dafny.NestedToken) { + var nt = (Dafny.NestedToken)tok; + ReportBplError(nt.Inner, "Related location", false, tw); + } + } + } + + class DafnyHelper { + private string fname; + private string source; + + private Dafny.Errors errors; + private Dafny.Program dafnyProgram; + private Bpl.Program boogieProgram; + + public DafnyHelper(string fname, string source) { + this.fname = fname; + this.source = source; + this.errors = new Dafny.Errors(); + } + + public bool Verify() { + return Parse() && Resolve() && Translate() && Boogie(); + } + + private bool Parse() { + Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); + Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); + var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && + Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); + if (success) { + dafnyProgram = new Dafny.Program(fname, module, builtIns); + } + return success; + } + + private bool Resolve() { + var resolver = new Dafny.Resolver(dafnyProgram); + resolver.ResolveProgram(dafnyProgram); + return resolver.ErrorCount == 0; + } + + private bool Translate() { + var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix + boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? + return true; + } + + private bool Boogie() { + if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? + ExecutionEngine.EliminateDeadVariables(boogieProgram); + ExecutionEngine.CollectModSets(boogieProgram); + ExecutionEngine.CoalesceBlocks(boogieProgram); + ExecutionEngine.Inline(boogieProgram); + + switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate + case PipelineOutcome.Done: + case PipelineOutcome.VerificationCompleted: + return true; + } + } + + return false; + } + } +} diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 0aac88b2..3da33f16 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -1,4 +1,4 @@ - + @@ -55,6 +55,9 @@ + + + @@ -72,4 +75,4 @@ --> - + \ No newline at end of file diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 660188ba..c6f619d3 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -10,116 +10,21 @@ using Bpl = Microsoft.Boogie; 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, ", ")); - } - } - } - - // FIXME: This should not be duplicated here - class DafnyConsolePrinter : ConsolePrinter { - public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { - // Dafny has 0-indexed columns, but Boogie counts from 1 - var realigned_tok = new Token(tok.line, tok.col - 1); - realigned_tok.kind = tok.kind; - realigned_tok.pos = tok.pos; - realigned_tok.val = tok.val; - realigned_tok.filename = tok.filename; - base.ReportBplError(realigned_tok, message, error, tw, category); - - if (tok is Dafny.NestedToken) { - var nt = (Dafny.NestedToken)tok; - ReportBplError(nt.Inner, "Related location", false, tw); - } - } - } - - [Serializable] - class VerificationTask { - [DataMember] - string[] args = null; - - [DataMember] - string filename = null; - - [DataMember] - string source = null; - - [DataMember] - bool sourceIsFile = false; - - string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } - - internal static VerificationTask ReadTask(string b64_repr) { - try { - var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); - using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { - DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); - return (VerificationTask)serializer.ReadObject(ms); - } - } catch (Exception ex) { - throw new ServerException("Deserialization failed: {0}.", ex.Message); - } - } - - internal static void SelfTest() { - var task = new VerificationTask() { - filename = "", - sourceIsFile = false, - args = new string[] { }, - source = "method selftest() { assert true; }" - }; - try { - task.Run(); - Interaction.EOM(Interaction.SUCCESS, null); - } catch (Exception ex) { - Interaction.EOM(Interaction.FAILURE, ex); - } - } - - internal void Run() { - Server.ApplyArgs(args); - new DafnyHelper(filename, ProgramSource).Verify(); - } - } - - class ServerException : Exception { - internal ServerException(string message) : base(message) { } - internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } - } - class Server { private bool running; static void Main(string[] args) { Server server = new Server(); - if (args.Length > 0) { - if (args[0] == "selftest") { - VerificationTask.SelfTest(); - } else if (File.Exists(args[0])) { - Console.SetIn(new StreamReader(args[0])); - server.Loop(); - } else { - Console.WriteLine("Not sure what to do with '{0}'", String.Join(" ", args)); - } + + var hasArg = args.Length > 0; + var arg = hasArg ? args[0] : null; + + if (hasArg && args[0] == "selftest") { + VerificationTask.SelfTest(); + } else if (hasArg && File.Exists(arg)) { + Console.WriteLine("# Reading from {0}", arg); + Console.SetIn(new StreamReader(arg)); + server.Loop(); } else { server.Loop(); } @@ -131,19 +36,6 @@ namespace Microsoft.Dafny { ExecutionEngine.printer = new DafnyConsolePrinter(); } - 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"); - } - } - void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine @@ -167,8 +59,10 @@ namespace Microsoft.Dafny { void Loop() { for (int cycle = 0; running; cycle++) { var line = Console.ReadLine() ?? "quit"; - var command = line.Split(); - Respond(command); + if (line != String.Empty && !line.StartsWith("#")) { + var command = line.Split(); + Respond(command); + } } } @@ -180,11 +74,11 @@ namespace Microsoft.Dafny { var verb = command[0]; if (verb == "verify") { - checkArgs(command, 0); + ServerUtils.checkArgs(command, 0); var payload = ReadPayload(); VerificationTask.ReadTask(payload).Run(); } else if (verb == "quit") { - checkArgs(command, 0); + ServerUtils.checkArgs(command, 0); Exit(); } else { throw new ServerException("Unknown verb '{0}'", verb); @@ -199,73 +93,9 @@ namespace Microsoft.Dafny { } } - 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); - } - } - void Exit() { this.running = false; } } - class DafnyHelper { - private string fname; - private string source; - - private Dafny.Errors errors; - private Dafny.Program dafnyProgram; - private Bpl.Program boogieProgram; - - public DafnyHelper(string fname, string source) { - this.fname = fname; - this.source = source; - this.errors = new Dafny.Errors(); - } - - public bool Verify() { - return Parse() && Resolve() && Translate() && Boogie(); - } - - private bool Parse() { - Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); - Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); - var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && - Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); - if (success) { - dafnyProgram = new Dafny.Program(fname, module, builtIns); - } - return success; - } - - private bool Resolve() { - var resolver = new Dafny.Resolver(dafnyProgram); - resolver.ResolveProgram(dafnyProgram); - return resolver.ErrorCount == 0; - } - - private bool Translate() { - var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix - boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? - return true; - } - - private bool Boogie() { - if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? - ExecutionEngine.EliminateDeadVariables(boogieProgram); - ExecutionEngine.CollectModSets(boogieProgram); - ExecutionEngine.CoalesceBlocks(boogieProgram); - ExecutionEngine.Inline(boogieProgram); - - switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate - case PipelineOutcome.Done: - case PipelineOutcome.VerificationCompleted: - return true; - } - } - - return false; - } - } } \ No newline at end of file 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"); + } + } + } +} diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs new file mode 100644 index 00000000..a00688b1 --- /dev/null +++ b/Source/DafnyServer/VerificationTask.cs @@ -0,0 +1,59 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using System.Text; +using System.Threading.Tasks; + +namespace Microsoft.Dafny { + [Serializable] + class VerificationTask { + [DataMember] + string[] args = null; + + [DataMember] + string filename = null; + + [DataMember] + string source = null; + + [DataMember] + bool sourceIsFile = false; + + string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } + + internal static VerificationTask ReadTask(string b64_repr) { + try { + var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); + using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { + DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); + return (VerificationTask)serializer.ReadObject(ms); + } + } catch (Exception ex) { + throw new ServerException("Deserialization failed: {0}.", ex.Message); + } + } + + internal static void SelfTest() { + var task = new VerificationTask() { + filename = "", + sourceIsFile = false, + args = new string[] { }, + source = "method selftest() { assert true; }" + }; + try { + task.Run(); + Interaction.EOM(Interaction.SUCCESS, null); + } catch (Exception ex) { + Interaction.EOM(Interaction.FAILURE, ex); + } + } + + internal void Run() { + ServerUtils.ApplyArgs(args); + new DafnyHelper(filename, ProgramSource).Verify(); + } + } +} -- cgit v1.2.3 From 0579ef0552cf496b7c7b2246586b91b5bb42d406 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 17:55:23 -0700 Subject: Integrate the DafnyServer project into the main Dafny solution --- Source/Dafny.sln | 17 +++++++++++++++++ Source/DafnyServer.sln | 20 -------------------- Source/DafnyServer/DafnyServer.csproj | 3 --- 3 files changed, 17 insertions(+), 23 deletions(-) delete mode 100644 Source/DafnyServer.sln (limited to 'Source/DafnyServer/DafnyServer.csproj') diff --git a/Source/Dafny.sln b/Source/Dafny.sln index e7ba8026..570922fa 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -5,6 +5,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver", "DafnyDriver\ EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline", "Dafny\DafnyPipeline.csproj", "{FE44674A-1633-4917-99F4-57635E6FA740}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyServer", "DafnyServer\DafnyServer.csproj", "{AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Checked|.NET = Checked|.NET @@ -52,6 +54,21 @@ Global {FE44674A-1633-4917-99F4-57635E6FA740}.Release|Any CPU.Build.0 = Release|Any CPU {FE44674A-1633-4917-99F4-57635E6FA740}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU {FE44674A-1633-4917-99F4-57635E6FA740}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Checked|.NET.ActiveCfg = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Checked|Any CPU.ActiveCfg = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Checked|Any CPU.Build.0 = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Checked|Mixed Platforms.Build.0 = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|.NET.ActiveCfg = Debug|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|Any CPU.Build.0 = Debug|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|.NET.ActiveCfg = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|Any CPU.ActiveCfg = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|Any CPU.Build.0 = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|Mixed Platforms.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/Source/DafnyServer.sln b/Source/DafnyServer.sln deleted file mode 100644 index 217b1c74..00000000 --- a/Source/DafnyServer.sln +++ /dev/null @@ -1,20 +0,0 @@ - -Microsoft Visual Studio Solution File, Format Version 12.00 -# Visual Studio 2012 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyServer", "DafnyServer\DafnyServer.csproj", "{AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Release|Any CPU = Release|Any CPU - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Debug|Any CPU.Build.0 = Debug|Any CPU - {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|Any CPU.ActiveCfg = Release|Any CPU - {AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}.Release|Any CPU.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 3da33f16..d1171d69 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -63,9 +63,6 @@ - - PreserveNewest - - \ No newline at end of file + -- cgit v1.2.3 From 69ed5bac5efbc0ac64f26b6dadf81bcfec9a0b5b Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 29 Sep 2015 17:45:10 +0200 Subject: Fix the build. --- Source/DafnyDriver/DafnyDriver.cs | 6 +++--- Source/DafnyServer/DafnyServer.csproj | 13 ++++++++----- 2 files changed, 11 insertions(+), 8 deletions(-) (limited to 'Source/DafnyServer/DafnyServer.csproj') diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index c45d66fc..8282edc7 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -226,8 +226,8 @@ namespace Microsoft.Dafny stats = new PipelineStatistics(); LinearTypeChecker ltc; - MoverTypeChecker mtc; - PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc, out mtc); + CivlTypeChecker ctc; + PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out ltc, out ctc); switch (oc) { case PipelineOutcome.Done: return oc; @@ -244,7 +244,7 @@ namespace Microsoft.Dafny fileNames.Add(bplFileName); Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true); if (reparsedProgram != null) { - ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc, out mtc); + ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName, out ltc, out ctc); } } return oc; diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 1a256f5f..af262fc3 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -1,4 +1,4 @@ - + @@ -84,9 +84,6 @@ - - ..\..\Binaries\DafnyPipeline.dll - @@ -99,6 +96,12 @@ + + + {fe44674a-1633-4917-99f4-57635e6fa740} + DafnyPipeline + + - + \ No newline at end of file -- cgit v1.2.3