From 4fc18b2fe45c9a29cb0b8fe93d3102cec9c83194 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 12 Oct 2010 00:13:50 +0000
Subject: Boogie: * enhanced the printing of captured states * addressed some
 warnings issued by VS 2010 * some code formatting

---
 Source/VCExpr/TypeErasure.cs | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

(limited to 'Source/VCExpr/TypeErasure.cs')

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index a33ea631..20c946e5 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -424,8 +424,8 @@ namespace Microsoft.Boogie.TypeErasure {
     public VCExprVar Typed2Untyped(VCExprVar var) {
       Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<VCExprVar>() != null);
-      VCExprVar res;
-      if (!Typed2UntypedVariables.TryGetValue(var, out res)) {
+      VCExprVar res = TryTyped2Untyped(var);
+      if (res == null) {
         res = Gen.Variable(var.Name, TypeAfterErasure(var.Type));
         Typed2UntypedVariables.Add(var, res);
         AddVarTypeAxiom(res, var.Type);
@@ -433,6 +433,23 @@ namespace Microsoft.Boogie.TypeErasure {
       return cce.NonNull(res);
     }
 
+    /// <summary>
+    ///  This method is like Typed2Untyped, except in the case where the given variables
+    ///  doesn't exist in the mapping.  For that case, this method returns null whereas
+    ///  Typed2Untyped creates a new variable that it adds to the mapping.
+    /// </summary>
+    /// <param name="var"></param>
+    /// <returns></returns>
+    public VCExprVar TryTyped2Untyped(VCExprVar var) {
+      Contract.Requires(var != null);
+      VCExprVar res;
+      if (Typed2UntypedVariables.TryGetValue(var, out res)) {
+        return res;
+      } else {
+        return null;
+      }
+    }
+
     protected abstract void AddVarTypeAxiom(VCExprVar/*!*/ var, Type/*!*/ originalType);
 
     ///////////////////////////////////////////////////////////////////////////
-- 
cgit v1.2.3