diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-06 09:28:53 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-06 09:28:53 -0800 |
| commit | 97bfe7a64d7b1fce0c3240e150d0150d65c34fe3 (patch) | |
| tree | a74d088dc8ae71b25678ecb06e26cdba0aebaf38 /Test | |
| parent | 1dcb9b3aa68245791e667f7354ada0dac1fbeddb (diff) | |
| parent | a24f6d113ae43115057a123b0fddff89ca709e1d (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/houdini/test9.bpl | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/Test/houdini/test9.bpl b/Test/houdini/test9.bpl new file mode 100644 index 00000000..24eb66e8 --- /dev/null +++ b/Test/houdini/test9.bpl @@ -0,0 +1,73 @@ +var v1: int;
+var v2: int;
+var v3: int;
+const{:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+const{:existential true} b5: bool;
+const{:existential true} b6: bool;
+const{:existential true} b7: bool;
+const{:existential true} b8: bool;
+const{:existential true} b9: bool;
+const{:existential true} b10: bool;
+const{:existential true} b11: bool;
+const{:existential true} b12: bool;
+const{:existential true} b13: bool;
+const{:existential true} b14: bool;
+const{:existential true} b15: bool;
+const{:existential true} b16: bool;
+
+procedure push()
+requires {:candidate} b1 ==> v1 == 0;
+requires {:candidate} b2 ==> v1 == 1;
+ensures {:candidate} b3 ==> v1 == 0;
+ensures {:candidate} b4 ==> v1 == 1;
+modifies v1,v2;
+{
+ v2 := v1;
+ v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5 ==> v1 == 0;
+requires {:candidate} b6 ==> v1 == 1;
+ensures {:candidate} b7 ==> v1 == 0;
+ensures {:candidate} b8 ==> v1 == 1;
+{
+ v1 := v2;
+ havoc v2;
+}
+
+procedure foo()
+modifies v1,v2;
+requires {:candidate} b9 ==> v1 == 0;
+requires {:candidate} b10 ==> v1 == 1;
+ensures {:candidate} b11 ==> v1 == 0;
+ensures {:candidate} b12 ==> v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13 ==> v1 == 0;
+requires {:candidate} b14 ==> v1 == 1;
+ensures {:candidate} b15 ==> v1 == 0;
+ensures {:candidate} b16 ==> v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure main()
+modifies v1,v2;
+{
+ v1 := 1;
+ call foo();
+ havoc v1;
+ call bar();
+}
+
|