diff options
| -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
|