diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-23 11:26:34 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-23 11:26:34 -0800 |
| commit | df1cd695daffb01a590a7310dbee1b6594de2ecd (patch) | |
| tree | e35d6d49291a2a89ba62647c23fd354ccbb81e25 /Test/houdini | |
| parent | 01c3e8e8045cfa8a2b5f0746897441ebf027749d (diff) | |
fixed bug in the inlineDepth option for houdini
small clean up in the inlining implementation
Diffstat (limited to 'Test/houdini')
| -rw-r--r-- | Test/houdini/Answer | 10 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 6 | ||||
| -rw-r--r-- | Test/houdini/test7.bpl | 15 | ||||
| -rw-r--r-- | Test/houdini/test8.bpl | 21 |
4 files changed, 52 insertions, 0 deletions
diff --git a/Test/houdini/Answer b/Test/houdini/Answer index 94ae7f04..60ae7d80 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -99,3 +99,13 @@ b6 = False b7 = False
Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- test7.bpl --------------------
+Assignment computed by Houdini:
+
+Boogie program verifier finished with 2 verified, 0 errors
+.
+-------------------- test8.bpl --------------------
+Assignment computed by Houdini:
+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index d0e53b08..40f8cea0 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -8,3 +8,9 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer %%f
)
+
+for %%f in (test7.bpl test8.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /inline:spec /inlineDepth:1 %%f
+)
diff --git a/Test/houdini/test7.bpl b/Test/houdini/test7.bpl new file mode 100644 index 00000000..b5c6a4c6 --- /dev/null +++ b/Test/houdini/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/houdini/test8.bpl b/Test/houdini/test8.bpl new file mode 100644 index 00000000..12eab481 --- /dev/null +++ b/Test/houdini/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 |