diff options
| author |  tabarbe <unknown> | 2010-08-20 00:53:31 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 00:53:31 +0000 |
| commit | 31c11cdcbcb3e82f4ed769de7e7d0d362f657a93 (patch) | |
| tree | 3467e04ca13ef66036052a26f2a21c7d1be5e14f /Source/VCExpr/TypeErasure.cs | |
| parent | c8e02f87038179ab575044c3e7eb00a2d5115389 (diff) | |
Boogie: Fixed some doubly-inherited-contract occurrences.
Diffstat (limited to 'Source/VCExpr/TypeErasure.cs')
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 5029ba53..f148dc79 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -655,10 +655,10 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null); }
return res;
}
-
+ [Pure]
public Function CastTo(Type type) {
Contract.Requires(type != null);
- Contract.Requires((UnchangedType(type)));
+ Contract.Requires(UnchangedType(type));
Contract.Ensures(Contract.Result<Function>() != null);
return GetTypeCasts(type).CastFromU;
}
|