From 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
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/AbsInt/AbsInt.csproj | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Source/AbsInt/AbsInt.csproj')

diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 454fc081..93d304d7 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -147,12 +147,16 @@
       <RequiredTargetFramework>3.5</RequiredTargetFramework>
     </Reference>
     <Reference Include="System.Data" />
+    <Reference Include="System.Numerics" />
     <Reference Include="System.Xml" />
   </ItemGroup>
   <ItemGroup>
     <Compile Include="AbstractInterpretation.cs" />
     <Compile Include="ExprFactories.cs" />
+    <Compile Include="IntervalDomain.cs" />
     <Compile Include="LoopInvariantsOnDemand.cs" />
+    <Compile Include="TrivialDomain.cs" />
+    <Compile Include="NativeLattice.cs" />
     <Compile Include="Traverse.cs" />
     <Compile Include="..\version.cs" />
   </ItemGroup>
-- 
cgit v1.2.3