Fixes

dafny-lang · Sep 24, 2024 · 6560fc2 · 6560fc2
1 parent 2eea9e3
commit 6560fc2
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 23 deletions.
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs
@@ -67,10 +67,16 @@ bool NeedsDefiniteAssignmentTracker(bool isGhost, Type type, bool isField) {
     void AddExistingDefiniteAssignmentTracker(IVariable p, bool forceGhostVar) {
       Contract.Requires(p != null);
 
-      if (NeedsDefiniteAssignmentTracker(p.IsGhost || forceGhostVar, p.Type, false)) {
-        var ie = new Bpl.IdentifierExpr(p.Tok, DefassPrefix + p.UniqueName, Bpl.Type.Bool);
-        DefiniteAssignmentTrackers.Add(p, ie);
+      if (DefiniteAssignmentTrackers.ContainsKey(p)) {
+        return;
       }
+
+      if (!NeedsDefiniteAssignmentTracker(p.IsGhost || forceGhostVar, p.Type, false)) {
+        return;
+      }
+
+      var ie = new Bpl.IdentifierExpr(p.Tok, DefassPrefix + p.UniqueName, Bpl.Type.Bool);
+      DefiniteAssignmentTrackers.Add(p, ie);
     }
 
     void AddDefiniteAssignmentTrackerSurrogate(Field field, TopLevelDeclWithMembers enclosingClass,

diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -1716,6 +1716,25 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
 
       GenerateMethodParameters(m.tok, m, kind, etran, inParams, out var outParams);
 
+
+      var name = MethodName(m, kind);
+      var req = GetRequires();
+      var mod = new List<Bpl.IdentifierExpr> { ordinaryEtran.HeapCastToIdentifierExpr };
+      var ens = GetEnsures();
+      var proc = new Bpl.Procedure(m.tok, name, new List<Bpl.TypeVariable>(),
+        inParams, outParams.Values.ToList(), false, req, mod, ens, etran.TrAttributes(m.Attributes, null));
+      AddVerboseNameAttribute(proc, m.FullDafnyName, kind);
+
+      if (InsertChecksums) {
+        InsertChecksum(m, proc, true);
+      }
+
+      currentModule = null;
+      codeContext = null;
+      isAllocContext = null;
+
+      return proc;
+
       List<Boogie.Requires> GetRequires() {
         var req = new List<Boogie.Requires>();
         // FREE PRECONDITIONS
@@ -1784,25 +1803,6 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
         return req;
       }
 
-
-      var name = MethodName(m, kind);
-      var req = GetRequires();
-      var mod = new List<Bpl.IdentifierExpr> { ordinaryEtran.HeapCastToIdentifierExpr };
-      var ens = GetEnsures();
-      var proc = new Bpl.Procedure(m.tok, name, new List<Bpl.TypeVariable>(),
-        inParams, outParams.Values.ToList(), false, req, mod, ens, etran.TrAttributes(m.Attributes, null));
-      AddVerboseNameAttribute(proc, m.FullDafnyName, kind);
-
-      if (InsertChecksums) {
-        InsertChecksum(m, proc, true);
-      }
-
-      currentModule = null;
-      codeContext = null;
-      isAllocContext = null;
-
-      return proc;
-
       List<Bpl.Ensures> GetEnsures() {
         var ens = new List<Bpl.Ensures>();
         if (kind is MethodTranslationKind.SpecWellformedness or MethodTranslationKind.OverrideCheck) {

diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs
@@ -37,7 +37,11 @@ public void SetCurrentDefinition(string verificationScopeId) {
     }
 
     public IEnumerable<ProofDependency> GetPotentialDependenciesForDefinition(string defName) {
-      return idsByMemberName[defName];
+      if (idsByMemberName.TryGetValue(defName, out var result)) {
+        return result;
+      }
+
+      return Enumerable.Empty<ProofDependency>();
     }
 
     public IEnumerable<ProofDependency> GetAllPotentialDependencies() {