diff options
Diffstat (limited to 'Test/inline')
33 files changed, 1648 insertions, 61 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer index 6a3f6ba7..88e3ed5f 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1,14 +1,14 @@ -------------------- test0.bpl --------------------
-test0.bpl(30,5): Error BP5001: This assertion might not hold.
+test0.bpl(32,5): Error BP5001: This assertion might not hold.
Execution trace:
- test0.bpl(26,3): anon0
- test0.bpl(30,5): anon3_Then
+ test0.bpl(28,3): anon0
+ test0.bpl(32,5): anon3_Then
Boogie program verifier finished with 1 verified, 1 error
-------------------- codeexpr.bpl --------------------
-codeexpr.bpl(40,5): Error BP5001: This assertion might not hold.
+codeexpr.bpl(42,5): Error BP5001: This assertion might not hold.
Execution trace:
- codeexpr.bpl(39,7): anon0
+ codeexpr.bpl(41,7): anon0
Boogie program verifier finished with 5 verified, 1 error
-------------------- test1.bpl --------------------
@@ -1455,12 +1455,12 @@ implementation bar() Boogie program verifier finished with 5 verified, 0 errors
-------------------- test5.bpl --------------------
-test5.bpl(37,3): Error BP5001: This assertion might not hold.
+test5.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- test5.bpl(34,10): anon0
- test5.bpl(28,10): inline$P$0$anon0
- test5.bpl(28,10): inline$P$1$anon0
- test5.bpl(34,10): anon0$2
+ test5.bpl(36,10): anon0
+ test5.bpl(30,10): inline$P$0$anon0
+ test5.bpl(30,10): inline$P$1$anon0
+ test5.bpl(36,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
-------------------- expansion3.bpl --------------------
@@ -1473,33 +1473,33 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-------------------- Elevator.bpl --------------------
-Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(18,3): anon0
+ Elevator.bpl(18,3): anon0$1
+ Elevator.bpl(19,3): anon10_LoopHead
+ Elevator.bpl(22,5): anon10_LoopBody
+ Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(27,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl with empty blocks --------------------
-Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(68,23): inline$Initialize$0$Entry
- Elevator.bpl(71,13): inline$Initialize$0$anon0
- Elevator.bpl(68,23): inline$Initialize$0$Return
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(19,5): anon11_Else
- Elevator.bpl(19,5): anon12_Else
- Elevator.bpl(24,7): anon13_Then
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(18,3): anon0
+ Elevator.bpl(71,23): inline$Initialize$0$Entry
+ Elevator.bpl(74,13): inline$Initialize$0$anon0
+ Elevator.bpl(71,23): inline$Initialize$0$Return
+ Elevator.bpl(18,3): anon0$1
+ Elevator.bpl(19,3): anon10_LoopHead
+ Elevator.bpl(22,5): anon10_LoopBody
+ Elevator.bpl(22,5): anon11_Else
+ Elevator.bpl(22,5): anon12_Else
+ Elevator.bpl(27,7): anon13_Then
+ Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry
+ Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(97,23): inline$MoveDown_Error$0$Return
+ Elevator.bpl(27,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- expansion2.bpl --------------------
@@ -1525,46 +1525,46 @@ function foo3(x: int) : bool; axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
Boogie program verifier finished with 0 verified, 0 errors
-fundef2.bpl(6,3): Error BP5001: This assertion might not hold.
+fundef2.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
- fundef2.bpl(5,3): anon0
+ fundef2.bpl(7,3): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- polyInline.bpl --------------------
-polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
-polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int
-polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
-polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
+polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(20,3): anon0
-polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
+ polyInline.bpl(23,3): anon0
+polyInline.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(27,3): anon0
+ polyInline.bpl(30,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
-polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
-polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int
-polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
-polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
+polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int
+polyInline.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(20,3): anon0
-polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
+ polyInline.bpl(23,3): anon0
+polyInline.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(27,3): anon0
+ polyInline.bpl(30,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
-------------------- InliningAndLoops.bpl --------------------
-InliningAndLoops.bpl(12,5): Error BP5001: This assertion might not hold.
+InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold.
Execution trace:
- InliningAndLoops.bpl(5,10): anon0#3
- InliningAndLoops.bpl(6,3): anon4_LoopHead#3
- InliningAndLoops.bpl(8,5): anon4_LoopBody#3
- InliningAndLoops.bpl(8,5): anon4_LoopBody$1#3
- InliningAndLoops.bpl(6,3): anon4_LoopHead#2
- InliningAndLoops.bpl(8,5): anon4_LoopBody#2
- InliningAndLoops.bpl(8,5): anon4_LoopBody$1#2
- InliningAndLoops.bpl(6,3): anon4_LoopHead#1
- InliningAndLoops.bpl(6,3): anon4_LoopDone#3
- InliningAndLoops.bpl(12,5): anon5_Then#3
+ InliningAndLoops.bpl(7,10): anon0#3
+ InliningAndLoops.bpl(8,3): anon4_LoopHead#3
+ InliningAndLoops.bpl(10,5): anon4_LoopBody#3
+ InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3
+ InliningAndLoops.bpl(8,3): anon4_LoopHead#2
+ InliningAndLoops.bpl(10,5): anon4_LoopBody#2
+ InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2
+ InliningAndLoops.bpl(8,3): anon4_LoopHead#1
+ InliningAndLoops.bpl(8,3): anon4_LoopDone#3
+ InliningAndLoops.bpl(14,5): anon5_Then#3
Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/inline/Elevator.bpl b/Test/inline/Elevator.bpl index 4ee1e997..7a6b8128 100644 --- a/Test/inline/Elevator.bpl +++ b/Test/inline/Elevator.bpl @@ -1,3 +1,6 @@ +// RUN: %boogie %s > %t
+// RUN: %boogie -removeEmptyBlocks:0 %s >> %t
+// RUN: %diff %s.expect %t
// A Boogie version of Elevator.asml (see Boogie/Test/inline/Elevator.asml)
var floors: [int]bool; // set of integer
diff --git a/Test/inline/Elevator.bpl.expect b/Test/inline/Elevator.bpl.expect new file mode 100644 index 00000000..87141605 --- /dev/null +++ b/Test/inline/Elevator.bpl.expect @@ -0,0 +1,28 @@ +Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Elevator.bpl(18,3): anon0 + Elevator.bpl(18,3): anon0$1 + Elevator.bpl(19,3): anon10_LoopHead + Elevator.bpl(22,5): anon10_LoopBody + Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0 + Elevator.bpl(27,7): anon13_Then$1 + +Boogie program verifier finished with 1 verified, 1 error +Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Elevator.bpl(18,3): anon0 + Elevator.bpl(71,23): inline$Initialize$0$Entry + Elevator.bpl(74,13): inline$Initialize$0$anon0 + Elevator.bpl(71,23): inline$Initialize$0$Return + Elevator.bpl(18,3): anon0$1 + Elevator.bpl(19,3): anon10_LoopHead + Elevator.bpl(22,5): anon10_LoopBody + Elevator.bpl(22,5): anon11_Else + Elevator.bpl(22,5): anon12_Else + Elevator.bpl(27,7): anon13_Then + Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry + Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0 + Elevator.bpl(97,23): inline$MoveDown_Error$0$Return + Elevator.bpl(27,7): anon13_Then$1 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl index 970591a5..a22fd18c 100644 --- a/Test/inline/InliningAndLoops.bpl +++ b/Test/inline/InliningAndLoops.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling %s > %t
+// RUN: %diff %s.expect %t
procedure foo(N: int)
requires N == 2;
{
diff --git a/Test/inline/InliningAndLoops.bpl.expect b/Test/inline/InliningAndLoops.bpl.expect new file mode 100644 index 00000000..b5c38542 --- /dev/null +++ b/Test/inline/InliningAndLoops.bpl.expect @@ -0,0 +1,14 @@ +InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold. +Execution trace: + InliningAndLoops.bpl(7,10): anon0#3 + InliningAndLoops.bpl(8,3): anon4_LoopHead#3 + InliningAndLoops.bpl(10,5): anon4_LoopBody#3 + InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3 + InliningAndLoops.bpl(8,3): anon4_LoopHead#2 + InliningAndLoops.bpl(10,5): anon4_LoopBody#2 + InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2 + InliningAndLoops.bpl(8,3): anon4_LoopHead#1 + InliningAndLoops.bpl(8,3): anon4_LoopDone#3 + InliningAndLoops.bpl(14,5): anon5_Then#3 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl index 67728ea5..f9cef515 100644 --- a/Test/inline/codeexpr.bpl +++ b/Test/inline/codeexpr.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
var g: bool;
procedure {:inline 1} bar() returns (l: bool)
diff --git a/Test/inline/codeexpr.bpl.expect b/Test/inline/codeexpr.bpl.expect new file mode 100644 index 00000000..b42164c8 --- /dev/null +++ b/Test/inline/codeexpr.bpl.expect @@ -0,0 +1,5 @@ +codeexpr.bpl(42,5): Error BP5001: This assertion might not hold. +Execution trace: + codeexpr.bpl(41,7): anon0 + +Boogie program verifier finished with 5 verified, 1 error diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl index b6ed19ed..da13d50f 100644 --- a/Test/inline/expansion2.bpl +++ b/Test/inline/expansion2.bpl @@ -1,3 +1,6 @@ +// RUN: %boogie -proverLog:%T/expand2.sx %s > %t
+// RUN: %diff %s.expect %t
+// RUN: %OutputCheck --file-to-check=%T/expand2.sx %s
function {:inline true} xxgz(x:int) returns(bool)
{ x > 0 }
function {:inline true} xxf1(x:int,y:bool) returns(int)
@@ -8,7 +11,9 @@ axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0); procedure foo()
{
+ // CHECK-NOT-L: xxgz
assert xxgz(12);
+ // CHECK-NOT-L: xxf1
assert xxf1(3,true) == 4;
}
diff --git a/Test/inline/expansion2.bpl.expect b/Test/inline/expansion2.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/inline/expansion2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl index 2b1f0caa..8d95166c 100644 --- a/Test/inline/expansion3.bpl +++ b/Test/inline/expansion3.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
function {:inline true} foo3(x:int, y:bool) returns(bool)
{ foo3(x,y) }
diff --git a/Test/inline/expansion3.bpl.expect b/Test/inline/expansion3.bpl.expect new file mode 100644 index 00000000..072e091a --- /dev/null +++ b/Test/inline/expansion3.bpl.expect @@ -0,0 +1,5 @@ +*** detected expansion loop on foo3 +*** detected expansion loop on foo3 +*** detected expansion loop on foo3 + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl index be11a391..c8bbe923 100644 --- a/Test/inline/expansion4.bpl +++ b/Test/inline/expansion4.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
function foo(x:int) : int
{ if x <= 0 then 1 else foo(x - 1) + 2 }
diff --git a/Test/inline/expansion4.bpl.expect b/Test/inline/expansion4.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/inline/expansion4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/inline/fundef.bpl b/Test/inline/fundef.bpl index 46ce65bd..a7298c9c 100644 --- a/Test/inline/fundef.bpl +++ b/Test/inline/fundef.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -print:- -env:0 %s > %t
+// RUN: %diff %s.expect %t
function {:inline true} foo(x:int) returns(bool)
{ x > 0 }
function {:inline false} foo2(x:int) returns(bool)
diff --git a/Test/inline/fundef.bpl.expect b/Test/inline/fundef.bpl.expect new file mode 100644 index 00000000..5adced6d --- /dev/null +++ b/Test/inline/fundef.bpl.expect @@ -0,0 +1,15 @@ + +function {:inline true} foo(x: int) : bool +{ + x > 0 +} + +function {:inline false} foo2(x: int) : bool; + +axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0)); + +function foo3(x: int) : bool; + +axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0)); + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/inline/fundef2.bpl b/Test/inline/fundef2.bpl index 2e005fcc..527d235d 100644 --- a/Test/inline/fundef2.bpl +++ b/Test/inline/fundef2.bpl @@ -1,7 +1,9 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
function {:inline true} foo(x:int) returns(bool)
{ x > 0 }
procedure P() {
assert foo(13);
assert foo(-5); // error
-}
\ No newline at end of file +}
diff --git a/Test/inline/fundef2.bpl.expect b/Test/inline/fundef2.bpl.expect new file mode 100644 index 00000000..f237e98a --- /dev/null +++ b/Test/inline/fundef2.bpl.expect @@ -0,0 +1,5 @@ +fundef2.bpl(8,3): Error BP5001: This assertion might not hold. +Execution trace: + fundef2.bpl(7,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/inline/polyInline.bpl b/Test/inline/polyInline.bpl index 320259bd..1f6ea200 100644 --- a/Test/inline/polyInline.bpl +++ b/Test/inline/polyInline.bpl @@ -1,3 +1,6 @@ +// RUN: %boogie /typeEncoding:predicates /logPrefix:p %s > %t
+// RUN: %boogie /typeEncoding:arguments /logPrefix:a %s >> %t
+// RUN: %diff %s.expect %t
const C:int;
const D:bool;
@@ -37,4 +40,4 @@ procedure Q() { assert giveEmpty3():bool == empty();
assert giveEmpty3() == C; // should not be provable
-}
\ No newline at end of file +}
diff --git a/Test/inline/polyInline.bpl.expect b/Test/inline/polyInline.bpl.expect new file mode 100644 index 00000000..e0fc093f --- /dev/null +++ b/Test/inline/polyInline.bpl.expect @@ -0,0 +1,22 @@ +polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int +polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int +polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int +polyInline.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + polyInline.bpl(23,3): anon0 +polyInline.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + polyInline.bpl(30,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors +polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int +polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int +polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int +polyInline.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + polyInline.bpl(23,3): anon0 +polyInline.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + polyInline.bpl(30,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/inline/test0.bpl b/Test/inline/test0.bpl index 1b46f8c7..9a547d77 100644 --- a/Test/inline/test0.bpl +++ b/Test/inline/test0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// inlined functions
function Twice(x: int) returns (int)
diff --git a/Test/inline/test0.bpl.expect b/Test/inline/test0.bpl.expect new file mode 100644 index 00000000..46485036 --- /dev/null +++ b/Test/inline/test0.bpl.expect @@ -0,0 +1,6 @@ +test0.bpl(32,5): Error BP5001: This assertion might not hold. +Execution trace: + test0.bpl(28,3): anon0 + test0.bpl(32,5): anon3_Then + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/inline/test1.bpl b/Test/inline/test1.bpl index db847b25..1414978b 100644 --- a/Test/inline/test1.bpl +++ b/Test/inline/test1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure Main()
{
diff --git a/Test/inline/test1.bpl.expect b/Test/inline/test1.bpl.expect new file mode 100644 index 00000000..7b796e50 --- /dev/null +++ b/Test/inline/test1.bpl.expect @@ -0,0 +1,191 @@ + +procedure Main(); + + + +implementation Main() +{ + var x: int; + var y: int; + + anon0: + x := 1; + y := 0; + call x := inc(x, 5); + call y := incdec(x, 2); + assert x - 1 == y; + return; +} + + + +procedure {:inline 1} incdec(x: int, y: int) returns (z: int); + ensures z == x + 1 - y; + + + +implementation {:inline 1} incdec(x: int, y: int) returns (z: int) +{ + + anon0: + z := x; + z := x + 1; + call z := dec(z, y); + return; +} + + + +procedure {:inline 1} inc(x: int, i: int) returns (y: int); + ensures y == x + i; + + + +implementation {:inline 1} inc(x: int, i: int) returns (y: int) +{ + + anon0: + y := x; + y := x + i; + return; +} + + + +procedure {:inline 1} dec(x: int, i: int) returns (y: int); + ensures y == x - i; + + + +implementation {:inline 1} dec(x: int, i: int) returns (y: int) +{ + + anon0: + y := x; + y := x - i; + return; +} + + +after inlining procedure calls +procedure Main(); + + +implementation Main() +{ + var x: int; + var y: int; + var inline$inc$0$x: int; + var inline$inc$0$i: int; + var inline$inc$0$y: int; + var inline$incdec$0$x: int; + var inline$incdec$0$y: int; + var inline$incdec$0$z: int; + var inline$dec$0$x: int; + var inline$dec$0$i: int; + var inline$dec$0$y: int; + + anon0: + x := 1; + y := 0; + goto inline$inc$0$Entry; + + inline$inc$0$Entry: + inline$inc$0$x := x; + inline$inc$0$i := 5; + havoc inline$inc$0$y; + goto inline$inc$0$anon0; + + inline$inc$0$anon0: + inline$inc$0$y := inline$inc$0$x; + inline$inc$0$y := inline$inc$0$x + inline$inc$0$i; + goto inline$inc$0$Return; + + inline$inc$0$Return: + assert inline$inc$0$y == inline$inc$0$x + inline$inc$0$i; + x := inline$inc$0$y; + goto anon0$1; + + anon0$1: + goto inline$incdec$0$Entry; + + inline$incdec$0$Entry: + inline$incdec$0$x := x; + inline$incdec$0$y := 2; + havoc inline$incdec$0$z; + goto inline$incdec$0$anon0; + + inline$incdec$0$anon0: + inline$incdec$0$z := inline$incdec$0$x; + inline$incdec$0$z := inline$incdec$0$x + 1; + goto inline$dec$0$Entry; + + inline$dec$0$Entry: + inline$dec$0$x := inline$incdec$0$z; + inline$dec$0$i := inline$incdec$0$y; + havoc inline$dec$0$y; + goto inline$dec$0$anon0; + + inline$dec$0$anon0: + inline$dec$0$y := inline$dec$0$x; + inline$dec$0$y := inline$dec$0$x - inline$dec$0$i; + goto inline$dec$0$Return; + + inline$dec$0$Return: + assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i; + inline$incdec$0$z := inline$dec$0$y; + goto inline$incdec$0$anon0$1; + + inline$incdec$0$anon0$1: + goto inline$incdec$0$Return; + + inline$incdec$0$Return: + assert inline$incdec$0$z == inline$incdec$0$x + 1 - inline$incdec$0$y; + y := inline$incdec$0$z; + goto anon0$2; + + anon0$2: + assert x - 1 == y; + return; +} + + +after inlining procedure calls +procedure {:inline 1} incdec(x: int, y: int) returns (z: int); + ensures z == x + 1 - y; + + +implementation {:inline 1} incdec(x: int, y: int) returns (z: int) +{ + var inline$dec$0$x: int; + var inline$dec$0$i: int; + var inline$dec$0$y: int; + + anon0: + z := x; + z := x + 1; + goto inline$dec$0$Entry; + + inline$dec$0$Entry: + inline$dec$0$x := z; + inline$dec$0$i := y; + havoc inline$dec$0$y; + goto inline$dec$0$anon0; + + inline$dec$0$anon0: + inline$dec$0$y := inline$dec$0$x; + inline$dec$0$y := inline$dec$0$x - inline$dec$0$i; + goto inline$dec$0$Return; + + inline$dec$0$Return: + assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i; + z := inline$dec$0$y; + goto anon0$1; + + anon0$1: + return; +} + + + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/inline/test2.bpl b/Test/inline/test2.bpl index a45e86d5..7cafdf62 100644 --- a/Test/inline/test2.bpl +++ b/Test/inline/test2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t
+// RUN: %diff %s.expect %t
var glb:int;
diff --git a/Test/inline/test2.bpl.expect b/Test/inline/test2.bpl.expect new file mode 100644 index 00000000..14521adb --- /dev/null +++ b/Test/inline/test2.bpl.expect @@ -0,0 +1,81 @@ + +var glb: int; + +procedure calculate(); + modifies glb; + + + +implementation calculate() +{ + var x: int; + var y: int; + + anon0: + y := 5; + call x := increase(y); + return; +} + + + +procedure {:inline 1} increase(i: int) returns (k: int); + modifies glb; + + + +implementation {:inline 1} increase(i: int) returns (k: int) +{ + var j: int; + + anon0: + j := i; + j := j + 1; + glb := glb + j; + k := j; + return; +} + + +after inlining procedure calls +procedure calculate(); + modifies glb; + + +implementation calculate() +{ + var x: int; + var y: int; + var inline$increase$0$j: int; + var inline$increase$0$i: int; + var inline$increase$0$k: int; + var inline$increase$0$glb: int; + + anon0: + y := 5; + goto inline$increase$0$Entry; + + inline$increase$0$Entry: + inline$increase$0$i := y; + havoc inline$increase$0$j, inline$increase$0$k; + inline$increase$0$glb := glb; + goto inline$increase$0$anon0; + + inline$increase$0$anon0: + inline$increase$0$j := inline$increase$0$i; + inline$increase$0$j := inline$increase$0$j + 1; + glb := glb + inline$increase$0$j; + inline$increase$0$k := inline$increase$0$j; + goto inline$increase$0$Return; + + inline$increase$0$Return: + x := inline$increase$0$k; + goto anon0$1; + + anon0$1: + return; +} + + + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/inline/test3.bpl b/Test/inline/test3.bpl index f705e7b0..3db73413 100644 --- a/Test/inline/test3.bpl +++ b/Test/inline/test3.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t
+// RUN: %diff %s.expect %t
var glb:int;
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 diff --git a/Test/inline/test4.bpl b/Test/inline/test4.bpl index 4a740bbc..248dfc6e 100644 --- a/Test/inline/test4.bpl +++ b/Test/inline/test4.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure main(x:int)
{
diff --git a/Test/inline/test4.bpl.expect b/Test/inline/test4.bpl.expect new file mode 100644 index 00000000..29f80858 --- /dev/null +++ b/Test/inline/test4.bpl.expect @@ -0,0 +1,332 @@ + +procedure main(x: int); + + + +implementation main(x: int) +{ + var A: [int]int; + var i: int; + var b: bool; + var size: int; + + anon0: + call i, b := find(A, size, x); + goto anon3_Then, anon3_Else; + + anon3_Then: + assume {:partition} b; + assert i > 0 && A[i] == x; + goto anon2; + + anon3_Else: + assume {:partition} !b; + goto anon2; + + anon2: + return; +} + + + +procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool); + + + +implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool) +{ + var i: int; + var b: bool; + + anon0: + ret := -1; + b := false; + found := b; + i := 0; + goto anon4_LoopHead; + + anon4_LoopHead: + goto anon4_LoopDone, anon4_LoopBody; + + anon4_LoopBody: + assume {:partition} i < size; + call b := check(A, i, x); + goto anon5_Then, anon5_Else; + + anon5_Then: + assume {:partition} b; + ret := i; + found := b; + goto anon3; + + anon5_Else: + assume {:partition} !b; + goto anon4_LoopHead; + + anon4_LoopDone: + assume {:partition} size <= i; + goto anon3; + + anon3: + return; +} + + + +procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool); + requires i >= 0; + ensures old(A[i]) > c ==> ret == true; + + + +implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool) +{ + + anon0: + goto anon4_Then, anon4_Else; + + anon4_Then: + assume {:partition} A[i] == c; + ret := true; + goto anon3; + + anon4_Else: + assume {:partition} A[i] != c; + ret := false; + goto anon3; + + anon3: + return; +} + + +after inlining procedure calls +procedure main(x: int); + + +implementation main(x: int) +{ + var A: [int]int; + var i: int; + var b: bool; + var size: int; + var inline$find$0$i: int; + var inline$find$0$b: bool; + var inline$find$0$A: [int]int; + var inline$find$0$size: int; + var inline$find$0$x: int; + var inline$find$0$ret: int; + var inline$find$0$found: bool; + var inline$check$0$A: [int]int; + var inline$check$0$i: int; + var inline$check$0$c: int; + var inline$check$0$ret: bool; + + anon0: + goto inline$find$0$Entry; + + inline$find$0$Entry: + inline$find$0$A := A; + inline$find$0$size := size; + inline$find$0$x := x; + havoc inline$find$0$i, inline$find$0$b, inline$find$0$ret, inline$find$0$found; + goto inline$find$0$anon0; + + inline$find$0$anon0: + inline$find$0$ret := -1; + inline$find$0$b := false; + inline$find$0$found := inline$find$0$b; + inline$find$0$i := 0; + goto inline$find$0$anon4_LoopHead; + + inline$find$0$anon4_LoopHead: + goto inline$find$0$anon4_LoopDone, inline$find$0$anon4_LoopBody; + + inline$find$0$anon4_LoopBody: + assume {:partition} inline$find$0$i < inline$find$0$size; + goto inline$check$0$Entry; + + inline$check$0$Entry: + inline$check$0$A := inline$find$0$A; + inline$check$0$i := inline$find$0$i; + inline$check$0$c := inline$find$0$x; + assert inline$check$0$i >= 0; + havoc inline$check$0$ret; + goto inline$check$0$anon0; + + inline$check$0$anon0: + goto inline$check$0$anon4_Then, inline$check$0$anon4_Else; + + inline$check$0$anon4_Else: + assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c; + inline$check$0$ret := false; + goto inline$check$0$anon3; + + inline$check$0$anon3: + goto inline$check$0$Return; + + inline$check$0$anon4_Then: + assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c; + inline$check$0$ret := true; + goto inline$check$0$anon3; + + inline$check$0$Return: + assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true); + inline$find$0$b := inline$check$0$ret; + goto inline$find$0$anon4_LoopBody$1; + + inline$find$0$anon4_LoopBody$1: + goto inline$find$0$anon5_Then, inline$find$0$anon5_Else; + + inline$find$0$anon5_Else: + assume {:partition} !inline$find$0$b; + goto inline$find$0$anon4_LoopHead; + + inline$find$0$anon5_Then: + assume {:partition} inline$find$0$b; + inline$find$0$ret := inline$find$0$i; + inline$find$0$found := inline$find$0$b; + goto inline$find$0$anon3; + + inline$find$0$anon3: + goto inline$find$0$Return; + + inline$find$0$anon4_LoopDone: + assume {:partition} inline$find$0$size <= inline$find$0$i; + goto inline$find$0$anon3; + + inline$find$0$Return: + i := inline$find$0$ret; + b := inline$find$0$found; + goto anon0$1; + + anon0$1: + goto anon3_Then, anon3_Else; + + anon3_Else: + assume {:partition} !b; + goto anon2; + + anon2: + return; + + anon3_Then: + assume {:partition} b; + assert i > 0 && A[i] == x; + goto anon2; +} + + +after inlining procedure calls +procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool); + + +implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool) +{ + var i: int; + var b: bool; + var inline$check$0$A: [int]int; + var inline$check$0$i: int; + var inline$check$0$c: int; + var inline$check$0$ret: bool; + + anon0: + ret := -1; + b := false; + found := b; + i := 0; + goto anon4_LoopHead; + + anon4_LoopHead: + goto anon4_LoopDone, anon4_LoopBody; + + anon4_LoopBody: + assume {:partition} i < size; + goto inline$check$0$Entry; + + inline$check$0$Entry: + inline$check$0$A := A; + inline$check$0$i := i; + inline$check$0$c := x; + assert inline$check$0$i >= 0; + havoc inline$check$0$ret; + goto inline$check$0$anon0; + + inline$check$0$anon0: + goto inline$check$0$anon4_Then, inline$check$0$anon4_Else; + + inline$check$0$anon4_Else: + assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c; + inline$check$0$ret := false; + goto inline$check$0$anon3; + + inline$check$0$anon3: + goto inline$check$0$Return; + + inline$check$0$anon4_Then: + assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c; + inline$check$0$ret := true; + goto inline$check$0$anon3; + + inline$check$0$Return: + assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true); + b := inline$check$0$ret; + goto anon4_LoopBody$1; + + anon4_LoopBody$1: + goto anon5_Then, anon5_Else; + + anon5_Else: + assume {:partition} !b; + goto anon4_LoopHead; + + anon5_Then: + assume {:partition} b; + ret := i; + found := b; + goto anon3; + + anon3: + return; + + anon4_LoopDone: + assume {:partition} size <= i; + goto anon3; +} + + +<console>(70,4): Error BP5003: A postcondition might not hold on this return path. +<console>(78,2): Related location: This is the postcondition that might not hold. +Execution trace: + <console>(19,0): anon0 + <console>(29,0): inline$find$0$anon0 + <console>(39,0): inline$find$0$anon4_LoopBody + <console>(43,0): inline$check$0$Entry + <console>(54,0): inline$check$0$anon4_Else + <console>(67,0): inline$check$0$Return +<console>(109,4): Error BP5001: This assertion might not hold. +Execution trace: + <console>(19,0): anon0 + <console>(29,0): inline$find$0$anon0 + <console>(39,0): inline$find$0$anon4_LoopBody + <console>(43,0): inline$check$0$Entry + <console>(62,0): inline$check$0$anon4_Then + <console>(67,0): inline$check$0$Return + <console>(79,0): inline$find$0$anon5_Then + <console>(107,0): anon3_Then +<console>(51,4): Error BP5003: A postcondition might not hold on this return path. +<console>(78,2): Related location: This is the postcondition that might not hold. +Execution trace: + <console>(10,0): anon0 + <console>(20,0): anon4_LoopBody + <console>(24,0): inline$check$0$Entry + <console>(35,0): inline$check$0$anon4_Else + <console>(48,0): inline$check$0$Return +<console>(99,0): Error BP5003: A postcondition might not hold on this return path. +<console>(78,2): Related location: This is the postcondition that might not hold. +Execution trace: + <console>(85,0): anon0 + <console>(93,0): anon4_Else + <console>(98,0): anon3 + +Boogie program verifier finished with 0 verified, 4 errors diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl index 6460232c..8e092261 100644 --- a/Test/inline/test5.bpl +++ b/Test/inline/test5.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// test a case, where the inlined proc comes before the caller
procedure {:inline 2} foo()
diff --git a/Test/inline/test5.bpl.expect b/Test/inline/test5.bpl.expect new file mode 100644 index 00000000..cd0530dd --- /dev/null +++ b/Test/inline/test5.bpl.expect @@ -0,0 +1,8 @@ +test5.bpl(39,3): Error BP5001: This assertion might not hold. +Execution trace: + test5.bpl(36,10): anon0 + test5.bpl(30,10): inline$P$0$anon0 + test5.bpl(30,10): inline$P$1$anon0 + test5.bpl(36,10): anon0$2 + +Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/inline/test6.bpl b/Test/inline/test6.bpl index 394be89e..febf1aae 100644 --- a/Test/inline/test6.bpl +++ b/Test/inline/test6.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure {:inline 2} foo()
modifies x;
{
diff --git a/Test/inline/test6.bpl.expect b/Test/inline/test6.bpl.expect new file mode 100644 index 00000000..240094e1 --- /dev/null +++ b/Test/inline/test6.bpl.expect @@ -0,0 +1,579 @@ + +procedure {:inline 2} foo(); + modifies x; + + + +implementation {:inline 2} foo() +{ + + anon0: + x := x + 1; + call foo(); + return; +} + + + +procedure {:inline 2} foo1(); + modifies x; + + + +implementation {:inline 2} foo1() +{ + + anon0: + x := x + 1; + call foo2(); + return; +} + + + +procedure {:inline 2} foo2(); + modifies x; + + + +implementation {:inline 2} foo2() +{ + + anon0: + x := x + 1; + call foo3(); + return; +} + + + +procedure {:inline 2} foo3(); + modifies x; + + + +implementation {:inline 2} foo3() +{ + + anon0: + x := x + 1; + call foo1(); + return; +} + + + +var x: int; + +procedure bar(); + modifies x; + + + +implementation bar() +{ + + anon0: + call foo(); + call foo1(); + return; +} + + +after inlining procedure calls +procedure {:inline 2} foo(); + modifies x; + + +implementation {:inline 2} foo() +{ + var inline$foo$0$x: int; + var inline$foo$1$x: int; + + anon0: + x := x + 1; + goto inline$foo$0$Entry; + + inline$foo$0$Entry: + inline$foo$0$x := x; + goto inline$foo$0$anon0; + + inline$foo$0$anon0: + x := x + 1; + goto inline$foo$1$Entry; + + inline$foo$1$Entry: + inline$foo$1$x := x; + goto inline$foo$1$anon0; + + inline$foo$1$anon0: + x := x + 1; + call foo(); + goto inline$foo$1$Return; + + inline$foo$1$Return: + goto inline$foo$0$anon0$1; + + inline$foo$0$anon0$1: + goto inline$foo$0$Return; + + inline$foo$0$Return: + goto anon0$1; + + anon0$1: + return; +} + + +after inlining procedure calls +procedure {:inline 2} foo1(); + modifies x; + + +implementation {:inline 2} foo1() +{ + var inline$foo2$0$x: int; + var inline$foo3$0$x: int; + var inline$foo1$0$x: int; + var inline$foo2$1$x: int; + var inline$foo3$1$x: int; + var inline$foo1$1$x: int; + + anon0: + x := x + 1; + goto inline$foo2$0$Entry; + + inline$foo2$0$Entry: + inline$foo2$0$x := x; + goto inline$foo2$0$anon0; + + inline$foo2$0$anon0: + x := x + 1; + goto inline$foo3$0$Entry; + + inline$foo3$0$Entry: + inline$foo3$0$x := x; + goto inline$foo3$0$anon0; + + inline$foo3$0$anon0: + x := x + 1; + goto inline$foo1$0$Entry; + + inline$foo1$0$Entry: + inline$foo1$0$x := x; + goto inline$foo1$0$anon0; + + inline$foo1$0$anon0: + x := x + 1; + goto inline$foo2$1$Entry; + + inline$foo2$1$Entry: + inline$foo2$1$x := x; + goto inline$foo2$1$anon0; + + inline$foo2$1$anon0: + x := x + 1; + goto inline$foo3$1$Entry; + + inline$foo3$1$Entry: + inline$foo3$1$x := x; + goto inline$foo3$1$anon0; + + inline$foo3$1$anon0: + x := x + 1; + goto inline$foo1$1$Entry; + + inline$foo1$1$Entry: + inline$foo1$1$x := x; + goto inline$foo1$1$anon0; + + inline$foo1$1$anon0: + x := x + 1; + call foo2(); + goto inline$foo1$1$Return; + + inline$foo1$1$Return: + goto inline$foo3$1$anon0$1; + + inline$foo3$1$anon0$1: + goto inline$foo3$1$Return; + + inline$foo3$1$Return: + goto inline$foo2$1$anon0$1; + + inline$foo2$1$anon0$1: + goto inline$foo2$1$Return; + + inline$foo2$1$Return: + goto inline$foo1$0$anon0$1; + + inline$foo1$0$anon0$1: + goto inline$foo1$0$Return; + + inline$foo1$0$Return: + goto inline$foo3$0$anon0$1; + + inline$foo3$0$anon0$1: + goto inline$foo3$0$Return; + + inline$foo3$0$Return: + goto inline$foo2$0$anon0$1; + + inline$foo2$0$anon0$1: + goto inline$foo2$0$Return; + + inline$foo2$0$Return: + goto anon0$1; + + anon0$1: + return; +} + + +after inlining procedure calls +procedure {:inline 2} foo2(); + modifies x; + + +implementation {:inline 2} foo2() +{ + var inline$foo3$0$x: int; + var inline$foo1$0$x: int; + var inline$foo2$0$x: int; + var inline$foo3$1$x: int; + var inline$foo1$1$x: int; + var inline$foo2$1$x: int; + + anon0: + x := x + 1; + goto inline$foo3$0$Entry; + + inline$foo3$0$Entry: + inline$foo3$0$x := x; + goto inline$foo3$0$anon0; + + inline$foo3$0$anon0: + x := x + 1; + goto inline$foo1$0$Entry; + + inline$foo1$0$Entry: + inline$foo1$0$x := x; + goto inline$foo1$0$anon0; + + inline$foo1$0$anon0: + x := x + 1; + goto inline$foo2$0$Entry; + + inline$foo2$0$Entry: + inline$foo2$0$x := x; + goto inline$foo2$0$anon0; + + inline$foo2$0$anon0: + x := x + 1; + goto inline$foo3$1$Entry; + + inline$foo3$1$Entry: + inline$foo3$1$x := x; + goto inline$foo3$1$anon0; + + inline$foo3$1$anon0: + x := x + 1; + goto inline$foo1$1$Entry; + + inline$foo1$1$Entry: + inline$foo1$1$x := x; + goto inline$foo1$1$anon0; + + inline$foo1$1$anon0: + x := x + 1; + goto inline$foo2$1$Entry; + + inline$foo2$1$Entry: + inline$foo2$1$x := x; + goto inline$foo2$1$anon0; + + inline$foo2$1$anon0: + x := x + 1; + call foo3(); + goto inline$foo2$1$Return; + + inline$foo2$1$Return: + goto inline$foo1$1$anon0$1; + + inline$foo1$1$anon0$1: + goto inline$foo1$1$Return; + + inline$foo1$1$Return: + goto inline$foo3$1$anon0$1; + + inline$foo3$1$anon0$1: + goto inline$foo3$1$Return; + + inline$foo3$1$Return: + goto inline$foo2$0$anon0$1; + + inline$foo2$0$anon0$1: + goto inline$foo2$0$Return; + + inline$foo2$0$Return: + goto inline$foo1$0$anon0$1; + + inline$foo1$0$anon0$1: + goto inline$foo1$0$Return; + + inline$foo1$0$Return: + goto inline$foo3$0$anon0$1; + + inline$foo3$0$anon0$1: + goto inline$foo3$0$Return; + + inline$foo3$0$Return: + goto anon0$1; + + anon0$1: + return; +} + + +after inlining procedure calls +procedure {:inline 2} foo3(); + modifies x; + + +implementation {:inline 2} foo3() +{ + var inline$foo1$0$x: int; + var inline$foo2$0$x: int; + var inline$foo3$0$x: int; + var inline$foo1$1$x: int; + var inline$foo2$1$x: int; + var inline$foo3$1$x: int; + + anon0: + x := x + 1; + goto inline$foo1$0$Entry; + + inline$foo1$0$Entry: + inline$foo1$0$x := x; + goto inline$foo1$0$anon0; + + inline$foo1$0$anon0: + x := x + 1; + goto inline$foo2$0$Entry; + + inline$foo2$0$Entry: + inline$foo2$0$x := x; + goto inline$foo2$0$anon0; + + inline$foo2$0$anon0: + x := x + 1; + goto inline$foo3$0$Entry; + + inline$foo3$0$Entry: + inline$foo3$0$x := x; + goto inline$foo3$0$anon0; + + inline$foo3$0$anon0: + x := x + 1; + goto inline$foo1$1$Entry; + + inline$foo1$1$Entry: + inline$foo1$1$x := x; + goto inline$foo1$1$anon0; + + inline$foo1$1$anon0: + x := x + 1; + goto inline$foo2$1$Entry; + + inline$foo2$1$Entry: + inline$foo2$1$x := x; + goto inline$foo2$1$anon0; + + inline$foo2$1$anon0: + x := x + 1; + goto inline$foo3$1$Entry; + + inline$foo3$1$Entry: + inline$foo3$1$x := x; + goto inline$foo3$1$anon0; + + inline$foo3$1$anon0: + x := x + 1; + call foo1(); + goto inline$foo3$1$Return; + + inline$foo3$1$Return: + goto inline$foo2$1$anon0$1; + + inline$foo2$1$anon0$1: + goto inline$foo2$1$Return; + + inline$foo2$1$Return: + goto inline$foo1$1$anon0$1; + + inline$foo1$1$anon0$1: + goto inline$foo1$1$Return; + + inline$foo1$1$Return: + goto inline$foo3$0$anon0$1; + + inline$foo3$0$anon0$1: + goto inline$foo3$0$Return; + + inline$foo3$0$Return: + goto inline$foo2$0$anon0$1; + + inline$foo2$0$anon0$1: + goto inline$foo2$0$Return; + + inline$foo2$0$Return: + goto inline$foo1$0$anon0$1; + + inline$foo1$0$anon0$1: + goto inline$foo1$0$Return; + + inline$foo1$0$Return: + goto anon0$1; + + anon0$1: + return; +} + + +after inlining procedure calls +procedure bar(); + modifies x; + + +implementation bar() +{ + var inline$foo$0$x: int; + var inline$foo$1$x: int; + var inline$foo1$0$x: int; + var inline$foo2$0$x: int; + var inline$foo3$0$x: int; + var inline$foo1$1$x: int; + var inline$foo2$1$x: int; + var inline$foo3$1$x: int; + + anon0: + goto inline$foo$0$Entry; + + inline$foo$0$Entry: + inline$foo$0$x := x; + goto inline$foo$0$anon0; + + inline$foo$0$anon0: + x := x + 1; + goto inline$foo$1$Entry; + + inline$foo$1$Entry: + inline$foo$1$x := x; + goto inline$foo$1$anon0; + + inline$foo$1$anon0: + x := x + 1; + call foo(); + goto inline$foo$1$Return; + + inline$foo$1$Return: + goto inline$foo$0$anon0$1; + + inline$foo$0$anon0$1: + goto inline$foo$0$Return; + + inline$foo$0$Return: + goto anon0$1; + + anon0$1: + goto inline$foo1$0$Entry; + + inline$foo1$0$Entry: + inline$foo1$0$x := x; + goto inline$foo1$0$anon0; + + inline$foo1$0$anon0: + x := x + 1; + goto inline$foo2$0$Entry; + + inline$foo2$0$Entry: + inline$foo2$0$x := x; + goto inline$foo2$0$anon0; + + inline$foo2$0$anon0: + x := x + 1; + goto inline$foo3$0$Entry; + + inline$foo3$0$Entry: + inline$foo3$0$x := x; + goto inline$foo3$0$anon0; + + inline$foo3$0$anon0: + x := x + 1; + goto inline$foo1$1$Entry; + + inline$foo1$1$Entry: + inline$foo1$1$x := x; + goto inline$foo1$1$anon0; + + inline$foo1$1$anon0: + x := x + 1; + goto inline$foo2$1$Entry; + + inline$foo2$1$Entry: + inline$foo2$1$x := x; + goto inline$foo2$1$anon0; + + inline$foo2$1$anon0: + x := x + 1; + goto inline$foo3$1$Entry; + + inline$foo3$1$Entry: + inline$foo3$1$x := x; + goto inline$foo3$1$anon0; + + inline$foo3$1$anon0: + x := x + 1; + call foo1(); + goto inline$foo3$1$Return; + + inline$foo3$1$Return: + goto inline$foo2$1$anon0$1; + + inline$foo2$1$anon0$1: + goto inline$foo2$1$Return; + + inline$foo2$1$Return: + goto inline$foo1$1$anon0$1; + + inline$foo1$1$anon0$1: + goto inline$foo1$1$Return; + + inline$foo1$1$Return: + goto inline$foo3$0$anon0$1; + + inline$foo3$0$anon0$1: + goto inline$foo3$0$Return; + + inline$foo3$0$Return: + goto inline$foo2$0$anon0$1; + + inline$foo2$0$anon0$1: + goto inline$foo2$0$Return; + + inline$foo2$0$Return: + goto inline$foo1$0$anon0$1; + + inline$foo1$0$anon0$1: + goto inline$foo1$0$Return; + + inline$foo1$0$Return: + goto anon0$2; + + anon0$2: + return; +} + + + +Boogie program verifier finished with 5 verified, 0 errors |