diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-29 14:43:03 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-29 14:43:03 -0800 |
| commit | 08e9539279d31cfb650e0e55984216f5c8ffcd25 (patch) | |
| tree | 66f9cb5a66bdb193a535dc9003dba0c2546a6441 /Source/VCGeneration/ConditionGeneration.cs | |
| parent | cc80320df0b652f25ffbd68a004b56c2ef34d981 (diff) | |
fixed problems with datatypes
removed stale contracts in stratified inlining
added test to datatypes
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 26361cdf..ed698d5f 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -25,12 +25,10 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(counterexample != null);
Contract.Invariant(cce.NonNullElements(args));
}
public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {
- Contract.Requires(cex != null);
Contract.Requires(cce.NonNullElements(x));
counterexample = cex;
args = x;
|