doomed stuff: minor bug fixes / improved output / more test cases

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;

+  }

+}