AbsHoudini: Added predicate-abstraction domain and some examples.

3 files changed, 59 insertions, 0 deletions

diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl
new file mode 100644
index 00000000..fc37a15b
--- /dev/null
+++ b/Test/AbsHoudini/pred1.bpl
@@ -0,0 +1,23 @@
+function {:existential true} b0(x:bool, y:bool): bool;

+function {:existential true} b1(x:bool, y:bool): bool;

+function {:existential true} b2(x:bool, y:bool): bool;

+

+var g: int;

+

+procedure main()

+modifies g;

+ensures b0(g == 0, g == 5);

+{

+  g := 0;

+  if(*) { g := 5; }

+  call foo();

+}

+

+procedure foo()

+  modifies g;

+  requires b1(g == 0, g == 5);

+  ensures b2(g == 0, g == 5);

+{

+  assume g != 5;

+}

+

diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl
new file mode 100644
index 00000000..3ce948ce
--- /dev/null
+++ b/Test/AbsHoudini/pred2.bpl
@@ -0,0 +1,12 @@
+function {:existential true} b0(x:bool): bool;

+

+var g: int;

+

+procedure main()

+modifies g;

+ensures b0(g == old(g));

+{

+  if(*) { g := 5; }

+  assume g != 5;

+}

+

diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl
new file mode 100644
index 00000000..450efde4
--- /dev/null
+++ b/Test/AbsHoudini/pred3.bpl
@@ -0,0 +1,24 @@
+function {:existential true} b0(x:bool, y:bool): bool;

+function {:existential true} b1(x:bool, y:bool): bool;

+function {:existential true} b2(x:bool, y:bool): bool;

+

+var g: int;

+

+procedure main()

+modifies g;

+ensures b0(g == 0, g == 5);

+{

+  assume 0 == old(g) || 1 == old(g);

+  g := 0;

+  if(*) { g := 5; }

+  call foo();

+}

+

+procedure foo()

+  modifies g;

+  requires b1(g == 0, g == 5);

+  ensures b2(old(g) == 0, old(g) == 5);

+{

+  assume g != 5;

+}

+