diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-21 08:14:39 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-21 08:14:39 -0800 |
| commit | 5dba06d46a3e8c044cd4cc2c254885da3ccc1bb2 (patch) | |
| tree | 6215386075ca00d6492c25972e5556318fe16bed /Test/houdini | |
| parent | c4d98c26f1b69f5bfc5590f742e06c25d002ad29 (diff) | |
forgot to check it in
Diffstat (limited to 'Test/houdini')
| -rw-r--r-- | Test/houdini/test10.bpl | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/Test/houdini/test10.bpl b/Test/houdini/test10.bpl new file mode 100644 index 00000000..abb993f7 --- /dev/null +++ b/Test/houdini/test10.bpl @@ -0,0 +1,47 @@ +var sdv_7: int;
+var sdv_21: int;
+const {:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+ sdv_21 := sdv_7;
+ sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := sdv_21;
+ havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1 ==> (sdv_7 == 0);
+ensures{:candidate} b2 ==> (sdv_7 == old(sdv_7));
+{
+ call push(2);
+ call pop();
+ call bar();
+}
+
+procedure bar()
+requires{:candidate} b3 ==> (sdv_7 == 0);
+ensures{:candidate} b4 ==> (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+ call push(1);
+ call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := 0;
+ call foo();
+}
+
|