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