diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-13 17:25:28 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-13 17:25:28 -0800 |
| commit | 163fc931061c2d3065ec7a0acba817357295c3d2 (patch) | |
| tree | 12184d064e2a169179c0285cd4c65adab41a7fcc /Test/inline | |
| parent | c6797daa49abefba4480e5e7c99ce1605edcb083 (diff) | |
added the option /inlineDepth:n. This option defaults to -1. If the user provides a non-negative number then that number is used to inline
procedures not annotated by {:inline n} attribute.
Diffstat (limited to 'Test/inline')
| -rw-r--r-- | Test/inline/Answer | 191 | ||||
| -rw-r--r-- | Test/inline/runtest.bat | 5 | ||||
| -rw-r--r-- | Test/inline/test7.bpl | 15 | ||||
| -rw-r--r-- | Test/inline/test8.bpl | 21 |
4 files changed, 232 insertions, 0 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer index ae632f79..2c29ab0b 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1439,6 +1439,197 @@ implementation bar() Boogie program verifier finished with 5 verified, 0 errors
+-------------------- test7.bpl --------------------
+
+var g: int;
+
+procedure main();
+ modifies g;
+
+
+
+implementation main()
+{
+
+ anon0:
+ g := 0;
+ call foo();
+ assert g == 1;
+ return;
+}
+
+
+
+procedure foo();
+ modifies g;
+
+
+
+implementation foo()
+{
+
+ anon0:
+ g := g + 1;
+ return;
+}
+
+
+after inlining procedure calls
+procedure main();
+ modifies g;
+
+
+implementation main()
+{
+ var inline$foo$0$g: int;
+
+ anon0:
+ g := 0;
+ goto inline$foo$0$Entry;
+
+ inline$foo$0$Entry:
+ inline$foo$0$g := g;
+ goto inline$foo$0$anon0;
+
+ inline$foo$0$anon0:
+ g := g + 1;
+ goto inline$foo$0$Return;
+
+ inline$foo$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ assert g == 1;
+ return;
+}
+
+
+
+Boogie program verifier finished with 2 verified, 0 errors
+-------------------- test8.bpl --------------------
+
+var g: int;
+
+procedure main();
+ modifies g;
+
+
+
+implementation main()
+{
+
+ anon0:
+ g := 0;
+ call foo();
+ assert g == 1;
+ return;
+}
+
+
+
+procedure {:inline 1} foo();
+ modifies g;
+
+
+
+implementation foo()
+{
+
+ anon0:
+ call bar();
+ return;
+}
+
+
+
+procedure bar();
+ modifies g;
+
+
+
+implementation bar()
+{
+
+ anon0:
+ g := g + 1;
+ return;
+}
+
+
+after inlining procedure calls
+procedure main();
+ modifies g;
+
+
+implementation main()
+{
+ var inline$foo$0$g: int;
+ var inline$bar$0$g: int;
+
+ anon0:
+ g := 0;
+ goto inline$foo$0$Entry;
+
+ inline$foo$0$Entry:
+ inline$foo$0$g := g;
+ goto inline$foo$0$anon0;
+
+ inline$foo$0$anon0:
+ goto inline$bar$0$Entry;
+
+ inline$bar$0$Entry:
+ inline$bar$0$g := g;
+ goto inline$bar$0$anon0;
+
+ inline$bar$0$anon0:
+ g := g + 1;
+ goto inline$bar$0$Return;
+
+ inline$bar$0$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:
+ assert g == 1;
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} foo();
+ modifies g;
+
+
+implementation foo()
+{
+ var inline$bar$0$g: int;
+
+ anon0:
+ goto inline$bar$0$Entry;
+
+ inline$bar$0$Entry:
+ inline$bar$0$g := g;
+ goto inline$bar$0$anon0;
+
+ inline$bar$0$anon0:
+ g := g + 1;
+ goto inline$bar$0$Return;
+
+ inline$bar$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+
+Boogie program verifier finished with 3 verified, 0 errors
-------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index f56d55a0..3a8b0a9d 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -13,6 +13,11 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do ( %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f
)
+for %%f in (test7.bpl test8.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /inline:spec /inlineDepth:1 /print:- /env:0 /printInlined /noinfer %%f
+)
+
for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
diff --git a/Test/inline/test7.bpl b/Test/inline/test7.bpl new file mode 100644 index 00000000..b5c6a4c6 --- /dev/null +++ b/Test/inline/test7.bpl @@ -0,0 +1,15 @@ +var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure foo()
+modifies g;
+{
+ g := g + 1;
+}
\ No newline at end of file diff --git a/Test/inline/test8.bpl b/Test/inline/test8.bpl new file mode 100644 index 00000000..12eab481 --- /dev/null +++ b/Test/inline/test8.bpl @@ -0,0 +1,21 @@ +var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure {:inline 1} foo()
+modifies g;
+{
+ call bar();
+}
+
+procedure bar()
+modifies g;
+{
+ g := g + 1;
+}
\ No newline at end of file |