diff options
Diffstat (limited to 'Test/smoke/smoke0.bpl')
-rw-r--r-- | Test/smoke/smoke0.bpl | 110 |
1 files changed, 55 insertions, 55 deletions
diff --git a/Test/smoke/smoke0.bpl b/Test/smoke/smoke0.bpl index 87531c8d..6c4c8167 100644 --- a/Test/smoke/smoke0.bpl +++ b/Test/smoke/smoke0.bpl @@ -1,55 +1,55 @@ -// RUN: %boogie -smoke "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-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;
- }
-}
-
-
+// RUN: %boogie -smoke "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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; + } +} + + |