diff options
Diffstat (limited to 'Test/doomed/notdoomed.bpl')
-rw-r--r-- | Test/doomed/notdoomed.bpl | 116 |
1 files changed, 58 insertions, 58 deletions
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl index 8d57db71..321cf1eb 100644 --- a/Test/doomed/notdoomed.bpl +++ b/Test/doomed/notdoomed.bpl @@ -1,58 +1,58 @@ -// RUN: %boogie -vc:doomed %s
-procedure a(x:int)
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
-procedure b(x:int)
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- assert false;
- }
-}
-
-
-procedure c(x:int)
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- assert {:PossiblyUnreachable} false;
- }
-}
-
-procedure useCE(x:int)
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- }
- if(x<7) {
- y := 5;
- } else {
- y := 6;
- }
-
-}
-
-
-
-
+// RUN: %boogie -vc:doomed %s +procedure a(x:int) +{ + var y : int; + + if(x<0) { + y := 1; + } else { + y := 2; + } +} + + +procedure b(x:int) +{ + var y : int; + + if(x<0) { + y := 1; + } else { + y := 2; + assert false; + } +} + + +procedure c(x:int) +{ + var y : int; + + if(x<0) { + y := 1; + } else { + y := 2; + assert {:PossiblyUnreachable} false; + } +} + +procedure useCE(x:int) +{ + var y : int; + + if(x<0) { + y := 1; + } else { + y := 2; + } + if(x<7) { + y := 5; + } else { + y := 6; + } + +} + + + + |