From 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 5 Dec 2011 23:07:06 -0800 Subject: Boogie: Added new abstract interpretation harness, which uses native Boogie Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred} --- Source/Core/AbsyCmd.cs | 1 + 1 file changed, 1 insertion(+) (limited to 'Source/Core/AbsyCmd.cs') diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 676ffd5a..06eb3ae5 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -800,6 +800,7 @@ namespace Microsoft.Boogie { }; // used by WidenPoints.Compute public VisitState TraversingStatus; + public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run public bool widenBlock; public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not -- cgit v1.2.3