From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/stratifiedinline/bar13.bpl | 72 ++++++++++++++++++++--------------------- 1 file changed, 36 insertions(+), 36 deletions(-) (limited to 'Test/stratifiedinline/bar13.bpl') diff --git a/Test/stratifiedinline/bar13.bpl b/Test/stratifiedinline/bar13.bpl index 7c8cc9bd..6447f622 100644 --- a/Test/stratifiedinline/bar13.bpl +++ b/Test/stratifiedinline/bar13.bpl @@ -1,36 +1,36 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; -} - +// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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; +} + -- cgit v1.2.3