diff options
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/doomed.bpl | 46 |
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;
+ }
+}
|