Boogie: Added stratified inlining. It is enabled using the flag /stratifiedInline:1.

1 files changed, 41 insertions, 0 deletions

diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl
new file mode 100644
index 00000000..7bd91184
--- /dev/null
+++ b/Test/stratifiedinline/bar3.bpl
@@ -0,0 +1,41 @@
+var y: int;

+var x: int;

+

+procedure {:inline 1} bar(b: bool)

+modifies y;

+{

+  if (b) {

+    y := y + 1;

+  } else {

+    y := y - 1;

+  }

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  var b: bool;

+  if (b) {

+    x := x + 1;

+    call bar(true);

+    call bar(true);

+    x := x + 1;

+  } else {

+    x := x - 1;

+    call bar(false);

+    call bar(false);

+    x := x - 1;  

+  }

+}

+

+

+procedure main()

+requires x == y;

+ensures x == y;

+modifies x, y;

+modifies y;

+{

+  call foo();

+  assert x == y;

+  call bar(false);

+}