From 241de8264a32285d371a53d8d91a219625d76922 Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Mon, 7 Mar 2011 05:15:14 +0000
Subject: Fix contracts so runtime checking can be turned on.

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

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

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 20c946e5..5f3dbc36 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -633,7 +633,7 @@ namespace Microsoft.Boogie.TypeErasure {
     protected VCExpr GenReverseCastEq(Function castToU, Function castFromU, out VCExprVar var, out List<VCTrigger/*!*/>/*!*/ triggers) {
       Contract.Requires((castFromU != null));
       Contract.Requires((castToU != null));
-      Contract.Requires((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));
+      Contract.Ensures((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));
       Contract.Ensures(Contract.ValueAtReturn(out var) != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
       var = Gen.Variable("x", U);
@@ -1588,7 +1588,7 @@ namespace Microsoft.Boogie.TypeErasure {
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(cce.NonNullElements(varsInCasts));
-      Contract.Invariant(cce.NonNullElements(varsOutsideCasts));
+      Contract.Invariant(varsOutsideCasts != null && Contract.ForAll(varsOutsideCasts, voc => voc.Key != null));
       Contract.Invariant(AxBuilder != null);
 
     }
-- 
cgit v1.2.3