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/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 9c721703..a2ad40f6 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -12,7 +12,6 @@ using System.Text;
 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 using Bpl = Microsoft.Boogie;

-using AI = Microsoft.AbstractInterpretationFramework;

 

 

 COMPILER BoogiePL

@@ -115,7 +114,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();} } }

 }

 

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