Removed AIFramework from Boogie -- use native trivial or native interval-based abstract interpretation instead.

Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie.
Command-line option '/logInfer' has been dropped.

1 files changed, 0 insertions, 2 deletions

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 69f505bc..e95bccda 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -6,7 +6,6 @@ using System.Text;
 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 using Bpl = Microsoft.Boogie;

-using AI = Microsoft.AbstractInterpretationFramework;

 

 

 

@@ -134,7 +133,6 @@ private class BvBounds : Expr {
     {Contract.Assert(false);throw new cce.UnreachableException();}

   }

   public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }

-  public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }

 }

 

 /*--------------------------------------------------------------------------*/