diff options
| author |  akashlal <unknown> | 2013-04-18 17:50:18 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-04-18 17:50:18 +0530 |
| commit | a2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 (patch) | |
| tree | 48d4d5b6d86968a058ffbbe9661518ec763b9204 /Test/AbsHoudini/test9.bpl | |
| parent | 308a4d37f063384cb8de166b248d9377c904e77c (diff) | |
Nice clean re-implementation of AbstractHoudini. And tests
Diffstat (limited to 'Test/AbsHoudini/test9.bpl')
| -rw-r--r-- | Test/AbsHoudini/test9.bpl | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl new file mode 100644 index 00000000..24eb66e8 --- /dev/null +++ b/Test/AbsHoudini/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();
+}
+
|