From 8cc5d9cc9d455b42fc19881f29da47a08f10d8e1 Mon Sep 17 00:00:00 2001
From: Unknown <akashl@akash-desk.fareast.corp.microsoft.com>
Date: Mon, 5 Nov 2012 15:52:27 +0530
Subject: Added Abstract Houdini: an implementation of Houdini based on
 abstract domains. Currently only predicate-abstraction domain is supported.

---
 Test/AbsHoudini/Answer      | 19 +++++++++++++++++++
 Test/AbsHoudini/f1.bpl      | 32 ++++++++++++++++++++++++++++++++
 Test/AbsHoudini/runtest.bat | 11 +++++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 Test/AbsHoudini/Answer
 create mode 100644 Test/AbsHoudini/f1.bpl
 create mode 100644 Test/AbsHoudini/runtest.bat

(limited to 'Test/AbsHoudini')

diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer
new file mode 100644
index 00000000..376d9f3a
--- /dev/null
+++ b/Test/AbsHoudini/Answer
@@ -0,0 +1,19 @@
+
+-------------------- f1.bpl --------------------
+Running Abstract Houdini
+	Post: g == old(g) + 1
+	Post: g == old(g) + 2
+	Post: g == old(g) + 3
+	Pre: old(g) == 0
+Trying summary for foo: (And (== (fooSummaryPred g g@0) false) (== (fooSummaryPred g g@0) false))
+Trying summary for foo: (And (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3))))) (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3))))))
+Trying summary for foo: (And (== (fooSummaryPred g g@0) (== g@0 (+ g 1))) (== (fooSummaryPred g g@0) (== g@0 (+ g 1))))
+Trying summary for main: (And (== (mainSummaryPred g g@3) false) (== (mainSummaryPred g g@3) false))
+Trying summary for main: (And (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3))))) (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3))))))
+Trying summary for main: (And (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1)))) (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1)))))
+Summary of main:
+(old(g) == 0 ==> g == old(g) + 1)
+Summary of foo:
+g == old(g) + 1
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl
new file mode 100644
index 00000000..5ea6797b
--- /dev/null
+++ b/Test/AbsHoudini/f1.bpl
@@ -0,0 +1,32 @@
+var g: int;
+
+procedure {:entrypoint} main()
+  modifies g;
+{
+   var x: int;
+   var c: bool;
+
+   g := 1;
+  
+   if(c) {
+     g := g + 1;
+   } else {
+     g := 3;
+   }
+
+   call foo();
+
+   if(old(g) == 0) { g := 1; }
+}
+
+procedure foo() 
+  modifies g;
+{
+  g := g + 1;
+}
+
+procedure {:template} summaryTemplate();
+  ensures g == old(g) + 1;
+  ensures g == old(g) + 2;
+  ensures g == old(g) + 3;
+  ensures {:pre} old(g) == 0;
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
new file mode 100644
index 00000000..34308e4e
--- /dev/null
+++ b/Test/AbsHoudini/runtest.bat
@@ -0,0 +1,11 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (f1.bpl) do (
+  echo.
+  echo -------------------- %%f --------------------
+  %BGEXE% %* /nologo /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f
+)
+
-- 
cgit v1.2.3