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/test21/MapOutputTypeParams.bpl | 76 ++++++++++++++++++------------------- 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'Test/test21/MapOutputTypeParams.bpl') diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl index c9304d34..484c7dc1 100644 --- a/Test/test21/MapOutputTypeParams.bpl +++ b/Test/test21/MapOutputTypeParams.bpl @@ -1,39 +1,39 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" -// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" -// RUN: %diff "%s.p.expect" "%t" -// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" -// RUN: %diff "%s.a.expect" "%t" - - - -var p : [int]a; - -procedure P() returns () modifies p; { - p[13] := 5; - p[17] := true; - p[13] := false; - p[17] := 8; - - assert p[13] == 5 && !p[13] && p[17] == 8 && p[17]; - assert p == p[28 := p]; // error -} - -var q : [int][a]b; - -procedure Q() returns () modifies q; { - q[17] := q[17][true := 13]; - q[17] := q[17][true := false]; - q[16] := q[17][true := 14]; - - assert q[17][true] == 13 && !q[17][true]; - assert q[17][true] == 14; // error -} - -procedure R() returns () modifies p; { - p[7] := 28; - p[5] := p[7]; - - assert p[7] == 28; - assert p[6] == 28; // error +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" + + + +var p : [int]a; + +procedure P() returns () modifies p; { + p[13] := 5; + p[17] := true; + p[13] := false; + p[17] := 8; + + assert p[13] == 5 && !p[13] && p[17] == 8 && p[17]; + assert p == p[28 := p]; // error +} + +var q : [int][a]b; + +procedure Q() returns () modifies q; { + q[17] := q[17][true := 13]; + q[17] := q[17][true := false]; + q[16] := q[17][true := 14]; + + assert q[17][true] == 13 && !q[17][true]; + assert q[17][true] == 14; // error +} + +procedure R() returns () modifies p; { + p[7] := 28; + p[5] := p[7]; + + assert p[7] == 28; + assert p[6] == 28; // error } \ No newline at end of file -- cgit v1.2.3