From 4fc18b2fe45c9a29cb0b8fe93d3102cec9c83194 Mon Sep 17 00:00:00 2001 From: rustanleino 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() != 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); } + /// + /// 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. + /// + /// + /// + 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