diff options
| author |  rustanleino <unknown> | 2010-10-09 04:30:35 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-10-09 04:30:35 +0000 |
| commit | 269dc18327a1398372b704918c0621117baad8f0 (patch) | |
| tree | 6970d9a4b37a4c7b54a789bad0e3a0c634f025bf /Source/VCGeneration | |
| parent | f177b27e36f8c45e554e93424bff20498f040f8c (diff) | |
Boogie: fixed a Code Contract in the source
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 48b982bf..9e68dc58 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -554,7 +554,7 @@ namespace VC { /// <param name="impl"></param>
public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<ErrorModel> errorsModel)
{
- Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
+ Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
List<Counterexample> errorsOut;
|