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/test0/SeparateVerification1.bpl | 42 ++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'Test/test0/SeparateVerification1.bpl') diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl index 5956828f..d06aa043 100644 --- a/Test/test0/SeparateVerification1.bpl +++ b/Test/test0/SeparateVerification1.bpl @@ -1,21 +1,21 @@ -// RUN: %boogie -noVerify "%s" SeparateVerification0.bpl > "%t" -// RUN: %diff "%s.expect" "%t" -// to be used with SeparateVerification0.bpl - -// x and y are declared in SeparateVerification0.bpl -axiom x + y <= 100; - -// these are declared as :extern as SeparateVerification0.bpl -type T; -const C: int; -function F(): int; -var n: int; -procedure P(); -procedure {:extern} Q(x: int); - -procedure Main() { - call P(); // note, calling the parameter-less non-extern P (an extern and a non-extern - // declaration of the same name are usually mostly identical declarations, - // but Boogie allows them to be different, because it ignores the extern ones) - call Q(); // ditto -} +// RUN: %boogie -noVerify "%s" SeparateVerification0.bpl > "%t" +// RUN: %diff "%s.expect" "%t" +// to be used with SeparateVerification0.bpl + +// x and y are declared in SeparateVerification0.bpl +axiom x + y <= 100; + +// these are declared as :extern as SeparateVerification0.bpl +type T; +const C: int; +function F(): int; +var n: int; +procedure P(); +procedure {:extern} Q(x: int); + +procedure Main() { + call P(); // note, calling the parameter-less non-extern P (an extern and a non-extern + // declaration of the same name are usually mostly identical declarations, + // but Boogie allows them to be different, because it ignores the extern ones) + call Q(); // ditto +} -- cgit v1.2.3