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/inline/test1.bpl | 92 +++++++++++++++++++++++++-------------------------- 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'Test/inline/test1.bpl') diff --git a/Test/inline/test1.bpl b/Test/inline/test1.bpl index 11ce6b4f..f9166965 100644 --- a/Test/inline/test1.bpl +++ b/Test/inline/test1.bpl @@ -1,47 +1,47 @@ -// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -procedure Main() -{ - - var x:int; - var y:int; - - x := 1; - y := 0; - - call x := inc(x, 5); - call y := incdec(x, 2); - - assert(x - 1 == y); - -} - -procedure {:inline 1} incdec(x:int, y:int) returns (z:int) - ensures z == x + 1 - y; -{ - z := x; - z := x + 1; - call z := dec(z, y); - - return; - -} - -procedure {:inline 1} inc(x:int, i:int) returns (y:int) - ensures y == x + i; -{ - y := x; - y := x + i; - return; - -} - -procedure {:inline 1} dec(x:int, i:int) returns (y:int) - ensures y == x - i; -{ - y := x; - y := x - i; - return; - +// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure Main() +{ + + var x:int; + var y:int; + + x := 1; + y := 0; + + call x := inc(x, 5); + call y := incdec(x, 2); + + assert(x - 1 == y); + +} + +procedure {:inline 1} incdec(x:int, y:int) returns (z:int) + ensures z == x + 1 - y; +{ + z := x; + z := x + 1; + call z := dec(z, y); + + return; + +} + +procedure {:inline 1} inc(x:int, i:int) returns (y:int) + ensures y == x + i; +{ + y := x; + y := x + i; + return; + +} + +procedure {:inline 1} dec(x:int, i:int) returns (y:int) + ensures y == x - i; +{ + y := x; + y := x - i; + return; + } \ No newline at end of file -- cgit v1.2.3