summaryrefslogtreecommitdiff
path: root/Source/AbsInt/NativeLattice.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AbsInt/NativeLattice.cs')
-rw-r--r--Source/AbsInt/NativeLattice.cs20
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);