Fix a few bugs

* Always have a set of IDs for a given procedure, even if empty.
* Don't consider `free ensures` and `assert true` to be goals.

Author: atomb

Source/Core/CoverageAnnotator.cs

@@ -17,9 +17,8 @@ public class CoverageAnnotator : StandardVisitor
   private Dictionary<string, ISet<string>> implementationGoalIds = new();
   private Dictionary<string, Absy> idMap = new();
 
-  private void addImplementationGoalId(string id)
+  private void AddImplementationGoalId(string id)
   {
-    implementationGoalIds.TryAdd(currentImplementation, new HashSet<string>());
     implementationGoalIds[currentImplementation].Add(id);
   }
 
@@ -30,7 +29,7 @@ private void AddId(ICarriesAttributes node, bool isGoal)
     Absy absy = node as Absy;
     idMap.Add(idStr, absy);
     if (isGoal) {
-      addImplementationGoalId(idStr);
+      AddImplementationGoalId(idStr);
     }
     node.AddStringAttribute(absy.tok, "id", idStr);
   }
@@ -53,11 +52,16 @@ private void AddId(ICarriesAttributes node, bool isGoal)
   public override Implementation VisitImplementation(Implementation node)
   {
     currentImplementation = node.Name;
+    implementationGoalIds.TryAdd(currentImplementation, new HashSet<string>());
     return base.VisitImplementation(node);
   }
 
   public override Cmd VisitAssertCmd(AssertCmd node)
   {
+    if (node.Expr is LiteralExpr {IsTrue: true}) {
+      return node;
+    }
+
     AddId(node, true);
     return base.VisitAssertCmd(node);
   }
@@ -82,6 +86,10 @@ public override Requires VisitRequires(Requires requires)
 
   public override Ensures VisitEnsures(Ensures ensures)
   {
+    if (ensures.Free) {
+      return ensures;
+    }
+
     AddId(ensures, true);
     return base.VisitEnsures(ensures);
   }