diff options
author | 2014-05-07 19:36:02 +0100 | |
---|---|---|
committer | 2014-05-07 19:36:02 +0100 | |
commit | 8702d84fd360d9c2f11da295d616af4738bfd09a (patch) | |
tree | b3900efaeec0ffc53ab1a8c4a7e826ec66bc086d /Test/inline/test3.bpl.expect | |
parent | 9f555ab92f7cfe9edab8f12277b27cdee1849c32 (diff) |
Enabled the inline lit tests. In order to support expansion2.bpl
we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.
Diffstat (limited to 'Test/inline/test3.bpl.expect')
-rw-r--r-- | Test/inline/test3.bpl.expect | 255 |
1 files changed, 255 insertions, 0 deletions
diff --git a/Test/inline/test3.bpl.expect b/Test/inline/test3.bpl.expect new file mode 100644 index 00000000..79545583 --- /dev/null +++ b/Test/inline/test3.bpl.expect @@ -0,0 +1,255 @@ + +var glb: int; + +procedure recursivetest(); + modifies glb; + + + +implementation recursivetest() +{ + + anon0: + glb := 5; + call glb := recursive(glb); + return; +} + + + +procedure {:inline 3} recursive(x: int) returns (y: int); + + + +implementation {:inline 3} recursive(x: int) returns (y: int) +{ + var k: int; + + anon0: + goto anon3_Then, anon3_Else; + + anon3_Then: + assume {:partition} x == 0; + y := 1; + return; + + anon3_Else: + assume {:partition} x != 0; + goto anon2; + + anon2: + call k := recursive(x - 1); + y := y + k; + return; +} + + +after inlining procedure calls +procedure recursivetest(); + modifies glb; + + +implementation recursivetest() +{ + var inline$recursive$0$k: int; + var inline$recursive$0$x: int; + var inline$recursive$0$y: int; + var inline$recursive$1$k: int; + var inline$recursive$1$x: int; + var inline$recursive$1$y: int; + var inline$recursive$2$k: int; + var inline$recursive$2$x: int; + var inline$recursive$2$y: int; + + anon0: + glb := 5; + goto inline$recursive$0$Entry; + + inline$recursive$0$Entry: + inline$recursive$0$x := glb; + havoc inline$recursive$0$k, inline$recursive$0$y; + goto inline$recursive$0$anon0; + + inline$recursive$0$anon0: + goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else; + + inline$recursive$0$anon3_Else: + assume {:partition} inline$recursive$0$x != 0; + goto inline$recursive$1$Entry; + + inline$recursive$1$Entry: + inline$recursive$1$x := inline$recursive$0$x - 1; + havoc inline$recursive$1$k, inline$recursive$1$y; + goto inline$recursive$1$anon0; + + inline$recursive$1$anon0: + goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else; + + inline$recursive$1$anon3_Else: + assume {:partition} inline$recursive$1$x != 0; + goto inline$recursive$2$Entry; + + inline$recursive$2$Entry: + inline$recursive$2$x := inline$recursive$1$x - 1; + havoc inline$recursive$2$k, inline$recursive$2$y; + goto inline$recursive$2$anon0; + + inline$recursive$2$anon0: + goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else; + + inline$recursive$2$anon3_Else: + assume {:partition} inline$recursive$2$x != 0; + call inline$recursive$2$k := recursive(inline$recursive$2$x - 1); + inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k; + goto inline$recursive$2$Return; + + inline$recursive$2$anon3_Then: + assume {:partition} inline$recursive$2$x == 0; + inline$recursive$2$y := 1; + goto inline$recursive$2$Return; + + inline$recursive$2$Return: + inline$recursive$1$k := inline$recursive$2$y; + goto inline$recursive$1$anon3_Else$1; + + inline$recursive$1$anon3_Else$1: + inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k; + goto inline$recursive$1$Return; + + inline$recursive$1$anon3_Then: + assume {:partition} inline$recursive$1$x == 0; + inline$recursive$1$y := 1; + goto inline$recursive$1$Return; + + inline$recursive$1$Return: + inline$recursive$0$k := inline$recursive$1$y; + goto inline$recursive$0$anon3_Else$1; + + inline$recursive$0$anon3_Else$1: + inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k; + goto inline$recursive$0$Return; + + inline$recursive$0$anon3_Then: + assume {:partition} inline$recursive$0$x == 0; + inline$recursive$0$y := 1; + goto inline$recursive$0$Return; + + inline$recursive$0$Return: + glb := inline$recursive$0$y; + goto anon0$1; + + anon0$1: + return; +} + + +after inlining procedure calls +procedure {:inline 3} recursive(x: int) returns (y: int); + + +implementation {:inline 3} recursive(x: int) returns (y: int) +{ + var k: int; + var inline$recursive$0$k: int; + var inline$recursive$0$x: int; + var inline$recursive$0$y: int; + var inline$recursive$1$k: int; + var inline$recursive$1$x: int; + var inline$recursive$1$y: int; + var inline$recursive$2$k: int; + var inline$recursive$2$x: int; + var inline$recursive$2$y: int; + + anon0: + goto anon3_Then, anon3_Else; + + anon3_Else: + assume {:partition} x != 0; + goto inline$recursive$0$Entry; + + inline$recursive$0$Entry: + inline$recursive$0$x := x - 1; + havoc inline$recursive$0$k, inline$recursive$0$y; + goto inline$recursive$0$anon0; + + inline$recursive$0$anon0: + goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else; + + inline$recursive$0$anon3_Else: + assume {:partition} inline$recursive$0$x != 0; + goto inline$recursive$1$Entry; + + inline$recursive$1$Entry: + inline$recursive$1$x := inline$recursive$0$x - 1; + havoc inline$recursive$1$k, inline$recursive$1$y; + goto inline$recursive$1$anon0; + + inline$recursive$1$anon0: + goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else; + + inline$recursive$1$anon3_Else: + assume {:partition} inline$recursive$1$x != 0; + goto inline$recursive$2$Entry; + + inline$recursive$2$Entry: + inline$recursive$2$x := inline$recursive$1$x - 1; + havoc inline$recursive$2$k, inline$recursive$2$y; + goto inline$recursive$2$anon0; + + inline$recursive$2$anon0: + goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else; + + inline$recursive$2$anon3_Else: + assume {:partition} inline$recursive$2$x != 0; + call inline$recursive$2$k := recursive(inline$recursive$2$x - 1); + inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k; + goto inline$recursive$2$Return; + + inline$recursive$2$anon3_Then: + assume {:partition} inline$recursive$2$x == 0; + inline$recursive$2$y := 1; + goto inline$recursive$2$Return; + + inline$recursive$2$Return: + inline$recursive$1$k := inline$recursive$2$y; + goto inline$recursive$1$anon3_Else$1; + + inline$recursive$1$anon3_Else$1: + inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k; + goto inline$recursive$1$Return; + + inline$recursive$1$anon3_Then: + assume {:partition} inline$recursive$1$x == 0; + inline$recursive$1$y := 1; + goto inline$recursive$1$Return; + + inline$recursive$1$Return: + inline$recursive$0$k := inline$recursive$1$y; + goto inline$recursive$0$anon3_Else$1; + + inline$recursive$0$anon3_Else$1: + inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k; + goto inline$recursive$0$Return; + + inline$recursive$0$anon3_Then: + assume {:partition} inline$recursive$0$x == 0; + inline$recursive$0$y := 1; + goto inline$recursive$0$Return; + + inline$recursive$0$Return: + k := inline$recursive$0$y; + goto anon3_Else$1; + + anon3_Else$1: + y := y + k; + return; + + anon3_Then: + assume {:partition} x == 0; + y := 1; + return; +} + + + +Boogie program verifier finished with 2 verified, 0 errors |