From eaf052fa512f87a16d16cbb6b4c78e7fbaaf85b8 Mon Sep 17 00:00:00 2001
From: schaef <unknown>
Date: Thu, 19 Nov 2009 13:47:20 +0000
Subject: doomed stuff: minor bug fixes / improved output / more test cases

---
 Test/doomed/doomed.bpl | 46 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 44 insertions(+), 2 deletions(-)

(limited to 'Test/doomed')

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;
+  }
+}
-- 
cgit v1.2.3