diff options
Diffstat (limited to 'Test/inline/test6.bpl')
-rw-r--r-- | Test/inline/test6.bpl | 78 |
1 files changed, 39 insertions, 39 deletions
diff --git a/Test/inline/test6.bpl b/Test/inline/test6.bpl index d2e034fc..386c8d94 100644 --- a/Test/inline/test6.bpl +++ b/Test/inline/test6.bpl @@ -1,39 +1,39 @@ -// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure {:inline 2} foo()
- modifies x;
-{
- x := x + 1;
- call foo();
-}
-
-procedure {:inline 2} foo1()
- modifies x;
-{
- x := x + 1;
- call foo2();
-}
-
-procedure {:inline 2} foo2()
- modifies x;
-{
- x := x + 1;
- call foo3();
-}
-
-procedure {:inline 2} foo3()
- modifies x;
-{
- x := x + 1;
- call foo1();
-}
-
-var x:int;
-
-procedure bar()
- modifies x;
-{
- call foo();
- call foo1();
-}
-
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure {:inline 2} foo() + modifies x; +{ + x := x + 1; + call foo(); +} + +procedure {:inline 2} foo1() + modifies x; +{ + x := x + 1; + call foo2(); +} + +procedure {:inline 2} foo2() + modifies x; +{ + x := x + 1; + call foo3(); +} + +procedure {:inline 2} foo3() + modifies x; +{ + x := x + 1; + call foo1(); +} + +var x:int; + +procedure bar() + modifies x; +{ + call foo(); + call foo1(); +} + |