Correct casing of variables

boogie-org · Oct 7, 2024 · eddcbba · eddcbba
1 parent 90ff1fa
commit eddcbba
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git a/Source/Core/AST/GotoBoogie/Block.cs b/Source/Core/AST/GotoBoogie/Block.cs
@@ -79,32 +79,32 @@ public int
   // This field is used during passification to null-out entries in block2Incarnation dictionary early
   public int succCount;
 
-  private HashSet<Variable /*!*/> _liveVarsBefore;
+  private HashSet<Variable /*!*/> liveVarsBefore;
 
-  public IEnumerable<Variable /*!*/> liveVarsBefore
+  public IEnumerable<Variable /*!*/> LiveVarsBefore
   {
     get
     {
       Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Variable /*!*/>>(), true));
-      if (this._liveVarsBefore == null)
+      if (this.liveVarsBefore == null)
       {
         return null;
       }
       else
       {
-        return this._liveVarsBefore.AsEnumerable<Variable>();
+        return this.liveVarsBefore.AsEnumerable<Variable>();
       }
     }
     set
     {
       Contract.Requires(cce.NonNullElements(value, true));
       if (value == null)
       {
-        this._liveVarsBefore = null;
+        this.liveVarsBefore = null;
       }
       else
       {
-        this._liveVarsBefore = new HashSet<Variable>(value);
+        this.liveVarsBefore = new HashSet<Variable>(value);
       }
     }
   }
@@ -114,18 +114,18 @@ void ObjectInvariant()
   {
     Contract.Invariant(this.label != null);
     Contract.Invariant(this.cmds != null);
-    Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true));
+    Contract.Invariant(cce.NonNullElements(this.liveVarsBefore, true));
   }
 
   public bool IsLive(Variable v)
   {
     Contract.Requires(v != null);
-    if (liveVarsBefore == null)
+    if (LiveVarsBefore == null)
     {
       return true;
     }
 
-    return liveVarsBefore.Contains(v);
+    return LiveVarsBefore.Contains(v);
   }
 
   public static Block ShallowClone(Block block) {
@@ -147,7 +147,7 @@ public Block(IToken tok, string /*!*/ label, List<Cmd> /*!*/ cmds, TransferCmd t
     this.cmds = cmds;
     this.TransferCmd = transferCmd;
     this.Predecessors = new List<Block>();
-    this._liveVarsBefore = null;
+    this.liveVarsBefore = null;
     this.TraversingStatus = VisitState.ToVisit;
     this.iterations = 0;
   }

diff --git a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs
@@ -20,7 +20,7 @@ public static void ClearLiveVariables(Implementation impl)
     foreach (Block /*!*/ block in impl.Blocks)
     {
       Contract.Assert(block != null);
-      block.liveVarsBefore = null;
+      block.LiveVarsBefore = null;
     }
   }
 
@@ -59,8 +59,8 @@ public void ComputeLiveVariables(Implementation impl)
           foreach (Block /*!*/ succ in gotoCmd.LabelTargets)
           {
             Contract.Assert(succ != null);
-            Contract.Assert(succ.liveVarsBefore != null);
-            liveVarsAfter.UnionWith(succ.liveVarsBefore);
+            Contract.Assert(succ.LiveVarsBefore != null);
+            liveVarsAfter.UnionWith(succ.LiveVarsBefore);
           }
         }
       }
@@ -84,7 +84,7 @@ public void ComputeLiveVariables(Implementation impl)
         Propagate(cmds[i], liveVarsAfter);
       }
 
-      block.liveVarsBefore = liveVarsAfter;
+      block.LiveVarsBefore = liveVarsAfter;
     }
   }
 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
@@ -764,7 +764,7 @@ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWr
         Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
 
         // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.
-        b.liveVarsBefore = null;
+        b.LiveVarsBefore = null;
 
         // Decrement the succCount field in each predecessor. Once the field reaches zero in any block,
         // all its successors have been passified.  Consequently, its entry in block2Incarnation can be removed.