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/bar13.bpl | |
parent | b59b35f382e3ee2b3fae1747bf783b808ad52ad8 (diff) |
and a test case
Diffstat (limited to 'Test/stratifiedinline/bar13.bpl')
-rw-r--r-- | Test/stratifiedinline/bar13.bpl | 34 |
1 files changed, 34 insertions, 0 deletions
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;
+}
+
|