From 48fed349a2fc592e7f015ecaa6cf98582446278f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 30 Jul 2015 17:43:13 -0700 Subject: Fix an issue where the server would reverify the same file multiple times. The confusing part here is that if one passes null as the ProgramId for two consecutive calls to Boogie, then Boogie will return the same results twice, regardless of what the second program was. --- Source/DafnyServer/Server.cs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'Source/DafnyServer') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 36c28627..660188ba 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -114,6 +114,9 @@ namespace Microsoft.Dafny { 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)); } @@ -248,15 +251,14 @@ namespace Microsoft.Dafny { return true; } - // FIXME var boogieFilename = Path.Combine(Path.GetTempPath(), Path.ChangeExtension(Path.GetFileName(fname), "bpl")); private bool Boogie() { - if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { + 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(), null, null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for programId and error delegate + 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; -- cgit v1.2.3