diff options
Diffstat (limited to 'Test/doomed/smoke0.bpl')
| -rw-r--r-- | Test/doomed/smoke0.bpl | 158 |
1 files changed, 79 insertions, 79 deletions
diff --git a/Test/doomed/smoke0.bpl b/Test/doomed/smoke0.bpl index db01233f..159244ab 100644 --- a/Test/doomed/smoke0.bpl +++ b/Test/doomed/smoke0.bpl @@ -1,79 +1,79 @@ -procedure a(x:int)
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
-procedure b(x:int)
- requires x>0;
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
-
-procedure c(x:int)
- requires x>0;
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- assert false;
- } else {
- y := 2;
- }
-}
-
-procedure d(x:int)
- requires x>0;
-{
- var y : int;
-
- if(x<0) {
- assert false;
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
-procedure doomed1(x:int)
-{
- var y : int;
- y := 0;
- if(x<0) {
- y := 1;
- } else {
- assert y!=0;
- }
-}
-
-
-procedure doomed2(x:int)
-{
- var y : int;
- y := 0;
- if(x!=0) {
- y := 1;
- } else {
- assert x!=0;
- }
-}
-
-
-
-
+procedure a(x:int) +{ + var y : int; + + if(x<0) { + y := 1; + } else { + y := 2; + } +} + + +procedure b(x:int) + requires x>0; +{ + var y : int; + + if(x<0) { + y := 1; + } else { + y := 2; + } +} + + + +procedure c(x:int) + requires x>0; +{ + var y : int; + + if(x<0) { + y := 1; + assert false; + } else { + y := 2; + } +} + +procedure d(x:int) + requires x>0; +{ + var y : int; + + if(x<0) { + assert false; + y := 1; + } else { + y := 2; + } +} + + +procedure doomed1(x:int) +{ + var y : int; + y := 0; + if(x<0) { + y := 1; + } else { + assert y!=0; + } +} + + +procedure doomed2(x:int) +{ + var y : int; + y := 0; + if(x!=0) { + y := 1; + } else { + assert x!=0; + } +} + + + + |