diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-24 14:22:33 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-24 14:22:33 -0800 |
| commit | 132b03c3c6032dd2db21eac27616f7212dbcbb52 (patch) | |
| tree | 21c8197f2c15c92a1b9ab65d6b0b926221975dc2 /Test/houdini/test1.bpl | |
| parent | df1cd695daffb01a590a7310dbee1b6594de2ecd (diff) | |
added some more statistics to houdini
added a coupe more regressions for houdini+inlineDepth
Diffstat (limited to 'Test/houdini/test1.bpl')
| -rw-r--r-- | Test/houdini/test1.bpl | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/Test/houdini/test1.bpl b/Test/houdini/test1.bpl new file mode 100644 index 00000000..e6ce06c9 --- /dev/null +++ b/Test/houdini/test1.bpl @@ -0,0 +1,36 @@ +var g: bool;
+
+procedure foo()
+modifies g;
+ensures b0 ==> (!old(g) ==> old(g) == g);
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g;
+ensures b1 ==> old(g) == g;
+{
+ g := true;
+}
+
+procedure ReleaseLock()
+modifies g;
+ensures b2 ==> old(g) == g;
+{
+ g := false;
+}
+
+procedure main()
+modifies g;
+{
+ g := false;
+ call foo();
+ assert !g;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
|