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, 9 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 4e9c5c10..1561aec0 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -339,15 +339,6 @@ namespace Microsoft.Boogie.VCExprAST {
 

     ///////////////////////////////////////////////////////////////////////////////////

 

-    public override AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {

-      //Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<AIVariableExpr>() != null);

-      Contract.Assert(false);

-      throw new cce.UnreachableException();

-    }

-

-    ///////////////////////////////////////////////////////////////////////////////////

-

     public override Expr VisitIdentifierExpr(IdentifierExpr node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Expr>() != null);