diff options
| author |  qadeer <unknown> | 2014-09-18 08:28:30 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-09-18 08:28:30 -0700 |
| commit | 0c35477ac7e7fb5b73b3c64e301e09cd876c0703 (patch) | |
| tree | 49d7e6a87d64ca0878103411328236701c36ec41 /Source/VCGeneration/ConditionGeneration.cs | |
| parent | 1f99baa7cd1bd3e8cdce7dcd854c416291d114a4 (diff) | |
fixed various CodeContracts issues.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
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) {
|