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, 17 insertions, 3 deletions

diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
index f5bf1e03..4fccc14b 100644
--- a/Source/AbsInt/NativeLattice.cs
+++ b/Source/AbsInt/NativeLattice.cs
@@ -6,6 +6,7 @@
 

 using System;

 using System.Collections.Generic;

+using System.Linq;

 using System.Text;

 using System.Diagnostics.Contracts;

 using Microsoft.Boogie;

@@ -95,7 +96,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       }

 

       if (lattice != null) {

-        Dictionary<Procedure, Implementation[]> procedureImplementations = AbstractionEngine.ComputeProcImplMap(program);

+        Dictionary<Procedure, Implementation[]> procedureImplementations = ComputeProcImplMap(program);

         ComputeProgramInvariants(program, procedureImplementations, lattice);

         if (CommandLineOptions.Clo.Ai.DebugStatistics) {

           Console.Error.WriteLine(lattice);

@@ -110,9 +111,22 @@ namespace Microsoft.Boogie.AbstractInterpretation
       }

     }

 

+    private static Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Program program) {

+      Contract.Requires(program != null);

+      // Since implementations call procedures (impl. signatures) 

+      // rather than directly calling other implementations, we first

+      // need to compute which implementations implement which

+      // procedures and remember which implementations call which

+      // procedures.

+

+      return program

+            .TopLevelDeclarations

+            .Where(d => d is Implementation).Select(i => (Implementation)i)

+            .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc);

+    }

+

     /// <summary>

-    /// Compute and apply the invariants for the program using the underlying abstract domain (using native Boogie

-    /// expressions, not the abstracted AI.Expr's).

+    /// Compute and apply the invariants for the program using the underlying abstract domain.

     /// </summary>

     public static void ComputeProgramInvariants(Program program, Dictionary<Procedure, Implementation[]> procedureImplementations, NativeLattice lattice) {

       Contract.Requires(program != null);