summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar schaef <unknown>2009-11-19 13:47:20 +0000
committerGravatar schaef <unknown>2009-11-19 13:47:20 +0000
commiteaf052fa512f87a16d16cbb6b4c78e7fbaaf85b8 (patch)
treef77c8514aa6c6ecbaed9b3c75d1815a79df1c67c /Test
parent62069bee7147d2f5ef620c0309ef1048ca95d0a7 (diff)
doomed stuff: minor bug fixes / improved output / more test cases
Diffstat (limited to 'Test')
-rw-r--r--Test/doomed/doomed.bpl46
1 files changed, 44 insertions, 2 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl
index a153e468..77eec249 100644
--- a/Test/doomed/doomed.bpl
+++ b/Test/doomed/doomed.bpl
@@ -1,5 +1,5 @@
-procedure a(x:int)
+procedure evilrequires(x:int)
requires x>0;
{
var y : int;
@@ -12,7 +12,7 @@ procedure a(x:int)
}
-procedure b(x:int)
+procedure evilbranch(x:int)
{
var y : int;
@@ -25,3 +25,45 @@ procedure b(x:int)
}
+procedure evilloop(x:int)
+{
+ var y : int;
+ y:=x;
+ while (y<100) {
+ y := y -1;
+ }
+}
+
+procedure evilpath(x:int)
+{
+ var y : int;
+ y:=0;
+ if (x>10) {
+ y:=3;
+ } else {
+ assert y!=0;
+ }
+}
+
+procedure evilcondition(x:int)
+{
+ var y : int;
+ y:=0;
+ if (x!=0) {
+ y:=3;
+ } else {
+ assert x!=0;
+ }
+}
+
+procedure evilensures(x:int) returns ($result: int)
+ ensures $result>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ $result:=-1;
+ }
+}