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, 6 insertions, 5 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 1653b723..75ba7372 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -20,7 +20,6 @@ namespace Microsoft.Boogie {
   using System.Diagnostics;

   using System.Linq;

   using VC;

-  using AI = Microsoft.AbstractInterpretationFramework;

   using BoogiePL = Microsoft.Boogie;

 

   /* 

@@ -583,11 +582,13 @@ namespace Microsoft.Boogie {
       // ---------- Infer invariants --------------------------------------------------------

 

       // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

-      if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) {

-        Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

-      } else {

-        Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

+      if (CommandLineOptions.Clo.UseAbstractInterpretation) {

+        if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial) {

+          // use /infer:j as the default

+          CommandLineOptions.Clo.Ai.J_Intervals = true;

+        }

       }

+      Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

 

       if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);