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/UpdateExpr.bpl | 166 +++++++++++++++++++++++----------------------- 1 file changed, 83 insertions(+), 83 deletions(-) (limited to 'Test/test2/UpdateExpr.bpl') diff --git a/Test/test2/UpdateExpr.bpl b/Test/test2/UpdateExpr.bpl index eb5ba2e1..fb858a44 100644 --- a/Test/test2/UpdateExpr.bpl +++ b/Test/test2/UpdateExpr.bpl @@ -1,83 +1,83 @@ -// RUN: %boogie -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -const a: [int]bool; - -// element 5 of a stores the value true -axiom a == a[5 := true]; - -procedure P() -{ - assert a[5]; -} - -procedure Q() -{ - assert a[4]; // error -} - -procedure R() -{ - assert !a[5]; // error -} - -procedure S(y: int, t: bool) - requires y <= 5; -{ - if (a[y := t][5] == false) { - assert y == 5; - } -} - -procedure T0(aa: [int,ref]bool) -{ - assert aa[5,null := true] != aa[2,null := false]; // error -} - -procedure T1(aa: [int,ref]bool) - requires aa[5,null] && !aa[2,null]; -{ - assert aa[5,null := true] == aa[2,null := false]; // error, because we have no extensionality -} - -procedure T2(aa: [int,ref]bool) - requires aa[5,null] && !aa[2,null]; -{ - assert (forall x: int, y: ref :: aa[5,null := true][x,y] == aa[2,null := false][x,y]); -} - -procedure U0(a: [int]int) -{ - var b: [int]int; - - b := a[5 := 12]; - assert a == b; // error -} - -procedure U1() returns (a: [int]int) -{ - var b: [int]int; - - b := a[5 := 12]; - a[5] := 12; - assert a == b; -} - -type Field a; -const unique IntField: Field int; -const unique RefField: Field ref; -const unique SomeField: Field int; - -procedure FieldProc(H: [ref,Field a]a, this: ref) -{ - var i: int, r: ref, y: any; - var K: [ref,Field a]a; - - K := H[this, IntField := 5][this, RefField := null][this, SomeField := 100][this, IntField := 7]; - assert K[this, IntField] == 7; - assert K[this, RefField] == null; - assert K[this, SomeField] == 100; -} - -type ref, any; -const null : ref; +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +const a: [int]bool; + +// element 5 of a stores the value true +axiom a == a[5 := true]; + +procedure P() +{ + assert a[5]; +} + +procedure Q() +{ + assert a[4]; // error +} + +procedure R() +{ + assert !a[5]; // error +} + +procedure S(y: int, t: bool) + requires y <= 5; +{ + if (a[y := t][5] == false) { + assert y == 5; + } +} + +procedure T0(aa: [int,ref]bool) +{ + assert aa[5,null := true] != aa[2,null := false]; // error +} + +procedure T1(aa: [int,ref]bool) + requires aa[5,null] && !aa[2,null]; +{ + assert aa[5,null := true] == aa[2,null := false]; // error, because we have no extensionality +} + +procedure T2(aa: [int,ref]bool) + requires aa[5,null] && !aa[2,null]; +{ + assert (forall x: int, y: ref :: aa[5,null := true][x,y] == aa[2,null := false][x,y]); +} + +procedure U0(a: [int]int) +{ + var b: [int]int; + + b := a[5 := 12]; + assert a == b; // error +} + +procedure U1() returns (a: [int]int) +{ + var b: [int]int; + + b := a[5 := 12]; + a[5] := 12; + assert a == b; +} + +type Field a; +const unique IntField: Field int; +const unique RefField: Field ref; +const unique SomeField: Field int; + +procedure FieldProc(H: [ref,Field a]a, this: ref) +{ + var i: int, r: ref, y: any; + var K: [ref,Field a]a; + + K := H[this, IntField := 5][this, RefField := null][this, SomeField := 100][this, IntField := 7]; + assert K[this, IntField] == 7; + assert K[this, RefField] == null; + assert K[this, SomeField] == 100; +} + +type ref, any; +const null : ref; -- cgit v1.2.3