diff options
| author |  tabarbe <unknown> | 2010-08-19 22:20:45 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-19 22:20:45 +0000 |
| commit | baaee0fe9402102ec86799c4e2c6304d5ebe4aa6 (patch) | |
| tree | 6b907f6f008e07dfd38df6d3ea0c916b0083b12f /Source/AbsInt | |
| parent | ef633e71d0b9baae12ea475281fa8a29c4329574 (diff) | |
Boogie: Removed an old task comment
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/AbstractInterpretation.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs index 946814ba..827bd070 100644 --- a/Source/AbsInt/AbstractInterpretation.cs +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -62,7 +62,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { public AbstractionEngine(AI.Lattice lattice) {
Contract.Requires(lattice != null);
- Contract.Assume(cce.IsExposable(log)); //TODO: use the extension method syntax //PM: One would need static class invariants to prove this property
+ Contract.Assume(cce.IsExposable(log)); //PM: One would need static class invariants to prove this property
cce.BeginExpose(log);
log.Enabled = AI.Lattice.LogSwitch;
cce.EndExpose();
@@ -420,7 +420,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { return fresh;
}
- private delegate CallSite/*!*/ MarkCallSite(AI.Lattice.Element/*!*/ currentValue);//TODO: Think this is an invariant, but not sure how2 deal with it
+ private delegate CallSite/*!*/ MarkCallSite(AI.Lattice.Element/*!*/ currentValue);
/// <summary>
/// Given a basic block, it propagates the abstract state at the entry point through the exit point of the block
|