diff options
| -rw-r--r-- | Test/stratifiedinline/Answer | 4 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar13.bpl | 34 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 3 |
3 files changed, 41 insertions, 0 deletions
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 -----
|