diff options
author | 2013-04-18 17:50:18 +0530 | |
---|---|---|
committer | 2013-04-18 17:50:18 +0530 | |
commit | a2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 (patch) | |
tree | 48d4d5b6d86968a058ffbbe9661518ec763b9204 /Test/AbsHoudini/houd10.bpl | |
parent | 308a4d37f063384cb8de166b248d9377c904e77c (diff) |
Nice clean re-implementation of AbstractHoudini. And tests
Diffstat (limited to 'Test/AbsHoudini/houd10.bpl')
-rw-r--r-- | Test/AbsHoudini/houd10.bpl | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl new file mode 100644 index 00000000..bb0c65e7 --- /dev/null +++ b/Test/AbsHoudini/houd10.bpl @@ -0,0 +1,22 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var fooVar: int;
+var xVar: int;
+
+procedure foo()
+modifies fooVar;
+modifies xVar;
+ensures b1() || fooVar==0;
+ensures b3() || xVar<0;
+{
+ fooVar:=5;
+ call bar();
+}
+
+procedure bar();
+modifies xVar;
+requires Assert() || fooVar!=5;
+
+// expected assigment: Assert->true,b1->True,b2->false,b3->True
|