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/test2.bpl | |
| parent | df1cd695daffb01a590a7310dbee1b6594de2ecd (diff) | |
added some more statistics to houdini
added a coupe more regressions for houdini+inlineDepth
Diffstat (limited to 'Test/houdini/test2.bpl')
| -rw-r--r-- | Test/houdini/test2.bpl | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/Test/houdini/test2.bpl b/Test/houdini/test2.bpl new file mode 100644 index 00000000..febb28e6 --- /dev/null +++ b/Test/houdini/test2.bpl @@ -0,0 +1,38 @@ +var g: int;
+var h: int;
+
+procedure foo()
+modifies g, h;
+ensures b0 ==> old(g) == g;
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g, h;
+ensures b1 ==> old(g) == g;
+{
+ h := g;
+ g := 1;
+}
+
+procedure ReleaseLock()
+modifies g, h;
+ensures b2 ==> old(g) == g;
+{
+ g := h;
+}
+
+procedure main()
+modifies g, h;
+{
+ g := 0;
+ call foo();
+ assert g == 0;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
|