From baaee0fe9402102ec86799c4e2c6304d5ebe4aa6 Mon Sep 17 00:00:00 2001 From: tabarbe <unknown> Date: Thu, 19 Aug 2010 22:20:45 +0000 Subject: Boogie: Removed an old task comment --- Source/AbsInt/AbstractInterpretation.cs | 4 ++-- 1 file 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 -- cgit v1.2.3