summaryrefslogtreecommitdiff
path: root/Test/inline/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/inline/Answer')
-rw-r--r--Test/inline/Answer588
1 files changed, 580 insertions, 8 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer
index c59772cd..d5a12321 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -880,6 +880,586 @@ Execution trace:
<console>(98,0): anon3
Boogie program verifier finished with 0 verified, 4 errors
+-------------------- test6.bpl --------------------
+
+procedure {:inline 2} foo();
+ modifies x;
+
+
+
+implementation foo()
+{
+
+ anon0:
+ x := x + 1;
+ call foo();
+ return;
+}
+
+
+
+procedure {:inline 2} foo1();
+ modifies x;
+
+
+
+implementation foo1()
+{
+
+ anon0:
+ x := x + 1;
+ call foo2();
+ return;
+}
+
+
+
+procedure {:inline 2} foo2();
+ modifies x;
+
+
+
+implementation foo2()
+{
+
+ anon0:
+ x := x + 1;
+ call foo3();
+ return;
+}
+
+
+
+procedure {:inline 2} foo3();
+ modifies x;
+
+
+
+implementation 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 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 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 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 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
-------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -894,14 +1474,6 @@ Execution trace:
test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
--------------------- test6.bpl --------------------
-test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
-test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
-test6.bpl(22,22): Error: the inlined procedure is recursive, call stack: foo3 -> foo1 -> foo2 -> foo3
-test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1
-test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
-test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1
-6 type checking errors detected in test6.bpl
-------------------- expansion.bpl --------------------
expansion.bpl(29,14): Error: invalid type for argument 0 in application of foo1: bool (expected: int)
expansion.bpl(13,16): Error: expansion: {:inline ...} expects either true or false as the argument
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-10 19:14:02 +0000