diff options
| author |  akashlal <unknown> | 2013-10-25 17:05:57 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-10-25 17:05:57 +0530 |
| commit | 6ac23081d4afe057d025edd9836a50020de475d2 (patch) | |
| tree | 4500a337d7f14338a36bcc8399770a67c531f429 /Test/stratifiedinline | |
| parent | b59b35f382e3ee2b3fae1747bf783b808ad52ad8 (diff) | |
and a test case
Diffstat (limited to 'Test/stratifiedinline')
| -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 -----
|