Cleanup a number of FIXMEs that I had left in the code

7 files changed, 19 insertions, 30 deletions

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?

     }

     /// <summary>

     /// 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<string, MemberDecl> 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

+    /// <summary>

+    /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms.

+    /// </summary>

     internal List<TriggerTerm> 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