diff options
| author |  qadeer <unknown> | 2013-08-15 11:26:09 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-08-15 11:26:09 -0700 |
| commit | 1ab4adb8ac3d6f5bd20801b2170c3f7bf00b8234 (patch) | |
| tree | 911173adede20c245215dd9c731076ded855c350 /Test/inline | |
| parent | 3219275e4d4fec086a171677df9164b8abd31423 (diff) | |
Extended codeexpr inlining to deal with nested codeexpr
Added a regression
Diffstat (limited to 'Test/inline')
| -rw-r--r-- | Test/inline/Answer | 6 | ||||
| -rw-r--r-- | Test/inline/codeexpr.bpl | 36 | ||||
| -rw-r--r-- | Test/inline/runtest.bat | 2 |
3 files changed, 43 insertions, 1 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer index b6207739..d1666e03 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -5,6 +5,12 @@ Execution trace: test0.bpl(30,5): anon3_Then
Boogie program verifier finished with 1 verified, 1 error
+-------------------- codeexpr.bpl --------------------
+codeexpr.bpl(35,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ codeexpr.bpl(34,7): anon0
+
+Boogie program verifier finished with 3 verified, 1 error
-------------------- test1.bpl --------------------
procedure Main();
diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl new file mode 100644 index 00000000..bd57329f --- /dev/null +++ b/Test/inline/codeexpr.bpl @@ -0,0 +1,36 @@ +var g: bool;
+
+procedure {:inline 1} bar() returns (l: bool)
+{
+ l := g;
+}
+
+procedure A1()
+modifies g;
+{
+ g := true;
+ assert |{ var l: bool; A: call l := bar(); return l; }|;
+ assert (exists p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);
+ assert (forall p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);
+}
+
+procedure A2()
+{
+ assert |{ var l: bool; A: assume g; call l := bar(); return l; }|;
+ assert g ==> |{ var l: bool; A: call l := bar(); return l; }|;
+ assert (exists p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);
+ assert (forall p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);
+}
+
+procedure A3()
+{
+ assume |{ var l: bool; A: call l := bar(); return l; }|;
+ assert |{ var l: bool; A: call l := bar(); return l; }|;
+}
+
+procedure A4()
+modifies g;
+{
+ g := true;
+ assert |{ var l: bool; A: call l := bar(); return !l; }|;
+}
\ No newline at end of file diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index cd404bfa..f025de1b 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -3,7 +3,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (test0.bpl) do (
+for %%f in (test0.bpl codeexpr.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
|