summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-09-18 08:28:30 -0700
committerGravatar qadeer <unknown>2014-09-18 08:28:30 -0700
commit0c35477ac7e7fb5b73b3c64e301e09cd876c0703 (patch)
tree49d7e6a87d64ca0878103411328236701c36ec41 /Source/VCGeneration/ConditionGeneration.cs
parent1f99baa7cd1bd3e8cdce7dcd854c416291d114a4 (diff)
fixed various CodeContracts issues.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs2
1 files changed, 0 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 81231fd0..d9f53a56 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -804,8 +804,6 @@ namespace VC {
Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(impl.Proc != null);
Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd);
- Contract.Ensures(Contract.Result<Block>() != null);
- Contract.Ensures(Contract.Result<Block>().TransferCmd is ReturnCmd);
TokenTextWriter debugWriter = null;
if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {