From 6ac23081d4afe057d025edd9836a50020de475d2 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Fri, 25 Oct 2013 17:05:57 +0530
Subject: and a test case

---
 Test/stratifiedinline/Answer      |  4 ++++
 Test/stratifiedinline/bar13.bpl   | 34 ++++++++++++++++++++++++++++++++++
 Test/stratifiedinline/runtest.bat |  3 +++
 3 files changed, 41 insertions(+)
 create mode 100644 Test/stratifiedinline/bar13.bpl

(limited to 'Test/stratifiedinline')

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index d2600aad..bed39837 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -509,3 +509,7 @@ Execution trace:
 
 Boogie program verifier finished with 0 verified, 1 error
 -----
+----- Running regression test bar13.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
diff --git a/Test/stratifiedinline/bar13.bpl b/Test/stratifiedinline/bar13.bpl
new file mode 100644
index 00000000..bdeaaa51
--- /dev/null
+++ b/Test/stratifiedinline/bar13.bpl
@@ -0,0 +1,34 @@
+var alloc: int;
+var assertsPassed: bool;
+procedure boogie_si_record_li2bpl_int(x: int);
+
+procedure __HAVOC_malloc(size: int) returns (ret: int);
+  free requires size >= 0;
+  modifies alloc;
+  free ensures ret == old(alloc);
+  free ensures alloc >= old(alloc) + size;
+
+
+procedure foo(arg: int) 
+  modifies alloc;
+{
+  var tt: int;
+
+  anon0__unique__1:
+    // assume NumberOfBytes_2 >= 0;
+    call boogie_si_record_li2bpl_int(arg);
+    call tt := __HAVOC_malloc(arg);
+    call boogie_si_record_li2bpl_int(alloc);
+    return;
+}
+
+procedure {:entrypoint} main()
+  modifies alloc;
+{
+  var t1: int;
+
+  assume alloc > 0;
+  call foo(t1);
+  assume alloc < 0;
+}
+
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index d4b9c811..eb5ff634 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -37,4 +37,7 @@ echo -----
 echo ----- Running regression test bar12.bpl
 %BGEXE% %* /stratifiedInline:1 /vc:i bar12.bpl
 echo -----
+echo ----- Running regression test bar13.bpl
+%BGEXE% %* /stratifiedInline:1 /vc:i bar13.bpl
+echo -----
 
-- 
cgit v1.2.3