inlining is now done in rhs of assignments for codeexprs

added more regressions

2 files changed, 28 insertions, 4 deletions

diff --git a/Test/inline/Answer b/Test/inline/Answer
index d1666e03..f08209e3 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -6,11 +6,11 @@ Execution trace:
 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- codeexpr.bpl --------------------

-codeexpr.bpl(35,5): Error BP5001: This assertion might not hold.

+codeexpr.bpl(40,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    codeexpr.bpl(34,7): anon0

+    codeexpr.bpl(39,7): anon0

 

-Boogie program verifier finished with 3 verified, 1 error

+Boogie program verifier finished with 5 verified, 1 error

 -------------------- test1.bpl --------------------

 

 procedure Main();

diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl
index bd57329f..67728ea5 100644
--- a/Test/inline/codeexpr.bpl
+++ b/Test/inline/codeexpr.bpl
@@ -5,6 +5,11 @@ procedure {:inline 1} bar() returns (l: bool)
   l := g;

 }

 

+procedure {:inline 1} baz() returns (l: bool)

+{

+  call l := bar();

+}

+

 procedure A1() 

 modifies g;

 {

@@ -33,4 +38,23 @@ modifies g;
 {

     g := true;

     assert |{ var l: bool; A: call l := bar(); return !l; }|;

-}
\ No newline at end of file
+}

+

+procedure A5() 

+modifies g;

+{

+    var m: bool;

+

+    g := true;

+    m := |{ var l: bool; A: call l := bar(); return l; }|;

+    assert m;

+}

+

+procedure A6() 

+modifies g;

+{

+    g := true;

+    assert |{ var l: bool; A: call l := baz(); return l; }|;

+    assert (exists p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);

+    assert (forall p: bool :: |{ var l: bool; A: call l := baz(); return l; }|);

+}