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/test2/ContractEvaluationOrder.bpl | 72 +++++++++++++++++----------------- 1 file changed, 36 insertions(+), 36 deletions(-) (limited to 'Test/test2/ContractEvaluationOrder.bpl') diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl index 8719dcfa..4115c4b0 100644 --- a/Test/test2/ContractEvaluationOrder.bpl +++ b/Test/test2/ContractEvaluationOrder.bpl @@ -1,36 +1,36 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure P() returns (x, y: int) - ensures x == y; // ensured by the body - ensures x == 0; // error: not ensured by the body - ensures y == 0; // follows from the previous two ensures clauses (provided they are - // indeed evaluated in this order, which they are supposed to be) -{ - x := y; -} - -procedure Q() returns (x, y: int) -{ - x := y; - - assert x == y; // ensured by the body - assert x == 0; // error: not ensured by the body - assert y == 0; // follows from the previous two asserts (provided they are - // indeed evaluated in this order, which they are supposed to be) -} - -procedure R() -{ - var a, b: int; - a := b; - call S(a, b); -} - -procedure S(x, y: int) - // In the call from R: - requires x == y; // ensured by the body of R - requires x == 0; // error: not ensured by the body of R - requires y == 0; // follows from the previous two requires clauses (provided they are - // indeed evaluated in this order, which they are supposed to be) -{ -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure P() returns (x, y: int) + ensures x == y; // ensured by the body + ensures x == 0; // error: not ensured by the body + ensures y == 0; // follows from the previous two ensures clauses (provided they are + // indeed evaluated in this order, which they are supposed to be) +{ + x := y; +} + +procedure Q() returns (x, y: int) +{ + x := y; + + assert x == y; // ensured by the body + assert x == 0; // error: not ensured by the body + assert y == 0; // follows from the previous two asserts (provided they are + // indeed evaluated in this order, which they are supposed to be) +} + +procedure R() +{ + var a, b: int; + a := b; + call S(a, b); +} + +procedure S(x, y: int) + // In the call from R: + requires x == y; // ensured by the body of R + requires x == 0; // error: not ensured by the body of R + requires y == 0; // follows from the previous two requires clauses (provided they are + // indeed evaluated in this order, which they are supposed to be) +{ +} -- cgit v1.2.3