summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-30 17:43:13 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-30 17:43:13 -0700
commit48fed349a2fc592e7f015ecaa6cf98582446278f (patch)
tree6a703769b5b244975df915a8af5c2edad4051d96 /Source
parent8c1a52e085aed20f62a5d24fb2af9bbd5cb3e469 (diff)
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.
Diffstat (limited to 'Source')
-rw-r--r--Source/DafnyServer/Server.cs8
1 files changed, 5 insertions, 3 deletions
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;