diff options
| author |  Rustan Leino <unknown> | 2014-02-10 18:14:46 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-10 18:14:46 -0800 |
| commit | 8567d68f7f04f87b2d4270e18713bdcdf4d26031 (patch) | |
| tree | 75e633b53ac24d35c2d8d51641736a6b6e22ac99 /Source/Core/Absy.cs | |
| parent | e2feccce72c3f6b6d7ef0ab6c82675e1ff86a5f1 (diff) | |
Fixed errors in the use of Code Contracts
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index f0e2e7ed..b220b373 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -783,7 +783,7 @@ namespace Microsoft.Boogie { public static Graph<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {
Contract.Requires(impl != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().TopologicalSort()));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().Nodes));
Contract.Ensures(Contract.Result<Graph<Block>>() != null);
Graph<Block/*!*/> g = new Graph<Block/*!*/>();
|