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/bitvectors/bv4.bpl | 50 ++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'Test/bitvectors/bv4.bpl') diff --git a/Test/bitvectors/bv4.bpl b/Test/bitvectors/bv4.bpl index 29c8130a..1e7b6e31 100644 --- a/Test/bitvectors/bv4.bpl +++ b/Test/bitvectors/bv4.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -function a() returns(bv32); -axiom a() == a(); - -axiom 0bv5 != 1bv5; - - -// ------------------------- -type $x; -function g() returns($x); -type Field x; -var $gmem : [ref, Field x] x; -const unique f : Field $x; - -procedure qq() - modifies $gmem; -{ - $gmem[null, f] := g(); -} - - -type ref; -const null : ref; +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function a() returns(bv32); +axiom a() == a(); + +axiom 0bv5 != 1bv5; + + +// ------------------------- +type $x; +function g() returns($x); +type Field x; +var $gmem : [ref, Field x] x; +const unique f : Field $x; + +procedure qq() + modifies $gmem; +{ + $gmem[null, f] := g(); +} + + +type ref; +const null : ref; -- cgit v1.2.3