diff options
| author |  wuestholz <unknown> | 2014-12-26 10:41:10 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-12-26 10:41:10 +0100 |
| commit | d41a7518de7fd135caf752824670723d06332298 (patch) | |
| tree | dc0f08bbcffd809fc5facbb7ecd5e8639d81ed43 /Source/VCGeneration/VC.cs | |
| parent | 71fc5f5b32a5939ad488d6070a6acaf4d7cb443a (diff) | |
Fixed a postcondition.
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b989c029..8a549e9d 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1156,7 +1156,7 @@ namespace VC { public static List<Split/*!*/> FindManualSplits(Implementation/*!*/ impl, Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, VCGen/*!*/ par) {
Contract.Requires(impl != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Split>>()));
+ Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
var splitPoints = new Dictionary<Block,int>();
foreach (var b in impl.Blocks) {
|