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/test1/MapsTypeErrors.bpl | 258 +++++++++++++++++++++--------------------- 1 file changed, 129 insertions(+), 129 deletions(-) (limited to 'Test/test1/MapsTypeErrors.bpl') diff --git a/Test/test1/MapsTypeErrors.bpl b/Test/test1/MapsTypeErrors.bpl index bedb02ec..4b1bfec6 100644 --- a/Test/test1/MapsTypeErrors.bpl +++ b/Test/test1/MapsTypeErrors.bpl @@ -1,129 +1,129 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var m: []int; -var p: []a; - -type ref; -const null: ref; - -procedure P() - requires m[] == 5; - modifies m; - modifies p; - ensures m[] == 30; - ensures p[] + p[] == 24; - ensures p[] == null; -{ - m[] := 12; - p[] := 12; - p[] := true; - assert p[] == m[]; - assert p[]; - m := m[:= 30]; - p := p[:=null]; -} - -procedure A() -{ - m[] := 12; // error: illegal assignment, because m is not in modifies clause -} - -procedure B() - modifies m; -{ - m := m[]; // type error - m[] := m; // type error -} - -procedure C() - modifies m; -{ - m[] := true; // type error -} - -// ----- - -procedure Genrc(x: int) returns (t: T); - -procedure Caller() returns (b: bool) -{ - var y: ref; - call y := Genrc(5); - b := y == null; -} - -// ---- - -type Field a; -type HeapType = [ref, Field a]a; -const F0: Field int; -const F1: Field bool; -const alloc: Field bool; -var Heap: HeapType; - -function LiberalEqual(a, b) returns (bool); -function StrictEqual(a,a) returns (bool); -function IntEqual(Field int,Field int) returns (bool); - -procedure FrameCondition(this: ref) - requires F0 == F1; // error - requires LiberalEqual(F0, F1); - requires StrictEqual(F0, F0); - requires StrictEqual(F0, F1); // error - modifies Heap; - ensures (forall o: ref, f: Field alpha :: - Heap[o,f] == old(Heap)[o,f] || - !old(Heap)[o,alloc] || - (o == this && StrictEqual(f, F0)) || // error: f and F0 don't have the same type - (o == this && LiberalEqual(f, f)) || - (o == this && IntEqual(F0, f)) // error: f and F0 don't have the same type - ); -{ -} - -// ---- bitvector inference ---- - -function Gimmie() returns (T); -function Same(T,T) returns (T); -procedure ConsumeAnything(t: T); - -procedure Bvs(x: bv31, y: int) returns (a: bv32) -{ - a := x[50 : 18]; // error - a := y[50 : 18]; // error - - a := Gimmie(); // fine, this can be made to have at least 32 bits - a := Gimmie()[50 : 18]; // fine, result is always 32 bits and Gimmie() can be made to have at least 50 bits - a := Gimmie()[50 : 17]; // error, result is 33 bits (but there's nothing wrong with Gimmie()) - - a := Gimmie() ++ Gimmie() ++ Gimmie(); - a := Gimmie() ++ Gimmie()[20:0]; - a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[27:0]; - a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[22:0]; - a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0] ++ Gimmie(); - a := Gimmie() ++ 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0]; - a := Same(Gimmie(), Gimmie()); - a := Same(Gimmie()[20:0], Gimmie()); // error, have only bv20, need bv32 - - a := Same(Gimmie() ++ Gimmie()[20:0], 0bv32); - a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()); - a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie() ++ Gimmie()); - a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()[40:30] ++ Gimmie()); - call ConsumeAnything(Same(Gimmie() ++ Gimmie()[20:0], 0bv18)); // error, can't make things smaller -} - -// ---- maps again ---- - -procedure Mmm() returns (a: [int,int]bool, b: HeapType, c: int) -{ - if (Gimmie()[null] == Gimmie()) { - a := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie()); - b := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie()); - a := Same(Gimmie()[Gimmie(), Gimmie() := 4], Gimmie()); // error - b := Same(Gimmie()[Gimmie(), Gimmie() := 5], Gimmie()); - b := Same(Gimmie()[Gimmie(), 6 := Gimmie()], Gimmie()); // error - } - c := Gimmie()[Gimmie() := 10][null]; - c := Gimmie()[Gimmie() := Gimmie()][null]; - c := Gimmie()[Gimmie() := false][null]; -} +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var m: []int; +var p: []a; + +type ref; +const null: ref; + +procedure P() + requires m[] == 5; + modifies m; + modifies p; + ensures m[] == 30; + ensures p[] + p[] == 24; + ensures p[] == null; +{ + m[] := 12; + p[] := 12; + p[] := true; + assert p[] == m[]; + assert p[]; + m := m[:= 30]; + p := p[:=null]; +} + +procedure A() +{ + m[] := 12; // error: illegal assignment, because m is not in modifies clause +} + +procedure B() + modifies m; +{ + m := m[]; // type error + m[] := m; // type error +} + +procedure C() + modifies m; +{ + m[] := true; // type error +} + +// ----- + +procedure Genrc(x: int) returns (t: T); + +procedure Caller() returns (b: bool) +{ + var y: ref; + call y := Genrc(5); + b := y == null; +} + +// ---- + +type Field a; +type HeapType = [ref, Field a]a; +const F0: Field int; +const F1: Field bool; +const alloc: Field bool; +var Heap: HeapType; + +function LiberalEqual(a, b) returns (bool); +function StrictEqual(a,a) returns (bool); +function IntEqual(Field int,Field int) returns (bool); + +procedure FrameCondition(this: ref) + requires F0 == F1; // error + requires LiberalEqual(F0, F1); + requires StrictEqual(F0, F0); + requires StrictEqual(F0, F1); // error + modifies Heap; + ensures (forall o: ref, f: Field alpha :: + Heap[o,f] == old(Heap)[o,f] || + !old(Heap)[o,alloc] || + (o == this && StrictEqual(f, F0)) || // error: f and F0 don't have the same type + (o == this && LiberalEqual(f, f)) || + (o == this && IntEqual(F0, f)) // error: f and F0 don't have the same type + ); +{ +} + +// ---- bitvector inference ---- + +function Gimmie() returns (T); +function Same(T,T) returns (T); +procedure ConsumeAnything(t: T); + +procedure Bvs(x: bv31, y: int) returns (a: bv32) +{ + a := x[50 : 18]; // error + a := y[50 : 18]; // error + + a := Gimmie(); // fine, this can be made to have at least 32 bits + a := Gimmie()[50 : 18]; // fine, result is always 32 bits and Gimmie() can be made to have at least 50 bits + a := Gimmie()[50 : 17]; // error, result is 33 bits (but there's nothing wrong with Gimmie()) + + a := Gimmie() ++ Gimmie() ++ Gimmie(); + a := Gimmie() ++ Gimmie()[20:0]; + a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[27:0]; + a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[22:0]; + a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0] ++ Gimmie(); + a := Gimmie() ++ 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0]; + a := Same(Gimmie(), Gimmie()); + a := Same(Gimmie()[20:0], Gimmie()); // error, have only bv20, need bv32 + + a := Same(Gimmie() ++ Gimmie()[20:0], 0bv32); + a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()); + a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie() ++ Gimmie()); + a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()[40:30] ++ Gimmie()); + call ConsumeAnything(Same(Gimmie() ++ Gimmie()[20:0], 0bv18)); // error, can't make things smaller +} + +// ---- maps again ---- + +procedure Mmm() returns (a: [int,int]bool, b: HeapType, c: int) +{ + if (Gimmie()[null] == Gimmie()) { + a := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie()); + b := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie()); + a := Same(Gimmie()[Gimmie(), Gimmie() := 4], Gimmie()); // error + b := Same(Gimmie()[Gimmie(), Gimmie() := 5], Gimmie()); + b := Same(Gimmie()[Gimmie(), 6 := Gimmie()], Gimmie()); // error + } + c := Gimmie()[Gimmie() := 10][null]; + c := Gimmie()[Gimmie() := Gimmie()][null]; + c := Gimmie()[Gimmie() := false][null]; +} -- cgit v1.2.3