From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Test/test20/Coercions.bpl | 38 +++++------ Test/test20/EmptySeq.bpl | 16 ++--- Test/test20/ParallelAssignment.bpl | 48 +++++++------- Test/test20/ParallelAssignment2.bpl | 24 +++---- Test/test20/PolyFuns0.bpl | 114 ++++++++++++++++----------------- Test/test20/PolyFuns1.bpl | 122 ++++++++++++++++++------------------ Test/test20/PolyPolyPoly.bpl | 48 +++++++------- Test/test20/PolyPolyPoly2.bpl | 70 ++++++++++----------- Test/test20/PolyProcs0.bpl | 70 ++++++++++----------- Test/test20/ProcParamReordering.bpl | 32 +++++----- Test/test20/Prog0.bpl | 74 +++++++++++----------- Test/test20/Prog1.bpl | 56 ++++++++--------- Test/test20/Prog2.bpl | 36 +++++------ Test/test20/TypeDecls0.bpl | 94 +++++++++++++-------------- Test/test20/TypeDecls1.bpl | 50 +++++++-------- Test/test20/TypeSynonyms0.bpl | 66 +++++++++---------- Test/test20/TypeSynonyms1.bpl | 98 ++++++++++++++--------------- Test/test20/TypeSynonyms2.bpl | 48 +++++++------- 18 files changed, 552 insertions(+), 552 deletions(-) (limited to 'Test/test20') diff --git a/Test/test20/Coercions.bpl b/Test/test20/Coercions.bpl index 0ad114a6..5487f33a 100644 --- a/Test/test20/Coercions.bpl +++ b/Test/test20/Coercions.bpl @@ -1,19 +1,19 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - -type C, D, E _; - -const x:int; -const c:C; -const d:D; - -axiom (x:int > 0); -axiom (x:int < 0); -axiom (x:E [a]int < 0); // impossible coercion - -axiom (c:D == d); // impossible coercion - -axiom (15:D == d); // impossible coercion -axiom (15:E int == d); // impossible coercion -axiom ((18*15):int == 0); +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +type C, D, E _; + +const x:int; +const c:C; +const d:D; + +axiom (x:int > 0); +axiom (x:int < 0); +axiom (x:E [a]int < 0); // impossible coercion + +axiom (c:D == d); // impossible coercion + +axiom (15:D == d); // impossible coercion +axiom (15:E int == d); // impossible coercion +axiom ((18*15):int == 0); diff --git a/Test/test20/EmptySeq.bpl b/Test/test20/EmptySeq.bpl index 2eeb9589..b1758acc 100644 --- a/Test/test20/EmptySeq.bpl +++ b/Test/test20/EmptySeq.bpl @@ -1,8 +1,8 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type Seq T; - -function Seq#Length(Seq T) returns (int); -function Seq#Empty() returns (Seq T); - -axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Seq T; + +function Seq#Length(Seq T) returns (int); +function Seq#Empty() returns (Seq T); + +axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); diff --git a/Test/test20/ParallelAssignment.bpl b/Test/test20/ParallelAssignment.bpl index d84b96ab..677bb476 100644 --- a/Test/test20/ParallelAssignment.bpl +++ b/Test/test20/ParallelAssignment.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// Examples from the Boogie2 language report -// (stuff where resolution succeeds, but typechecking might fail) - -type C, D; - -var x : int; -var y : int; -var z : int; -var a : [int]int; -var b : [int][C, D]int; - -procedure P(i:int, j:int, m:C, n:D) returns () modifies x, y, a, b; { - x := x+1; - a[i] := 12; - x, y := y, x; - x, a[i] := x+1, x; - x := true; // type error - a[true] := 5; // type error - - z := 23; // assignment to non-modifiable variable - b[i][m, n] := 17; - b[i][m, n], x := a[x], y; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Examples from the Boogie2 language report +// (stuff where resolution succeeds, but typechecking might fail) + +type C, D; + +var x : int; +var y : int; +var z : int; +var a : [int]int; +var b : [int][C, D]int; + +procedure P(i:int, j:int, m:C, n:D) returns () modifies x, y, a, b; { + x := x+1; + a[i] := 12; + x, y := y, x; + x, a[i] := x+1, x; + x := true; // type error + a[true] := 5; // type error + + z := 23; // assignment to non-modifiable variable + b[i][m, n] := 17; + b[i][m, n], x := a[x], y; } \ No newline at end of file diff --git a/Test/test20/ParallelAssignment2.bpl b/Test/test20/ParallelAssignment2.bpl index 8f309b75..df9e5655 100644 --- a/Test/test20/ParallelAssignment2.bpl +++ b/Test/test20/ParallelAssignment2.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// Examples from the Boogie2 language report -// (examples where already resolution fails) - -var x : int; -var y : int; -var a : [int]int; - -procedure P(i:int, j:int) returns () modifies x, y, a; { - x, y := 1; // wrong number of rhss - a[i], a[j] := a[j], a[i]; // variable assigned more than once +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Examples from the Boogie2 language report +// (examples where already resolution fails) + +var x : int; +var y : int; +var a : [int]int; + +procedure P(i:int, j:int) returns () modifies x, y, a; { + x, y := 1; // wrong number of rhss + a[i], a[j] := a[j], a[i]; // variable assigned more than once } \ No newline at end of file diff --git a/Test/test20/PolyFuns0.bpl b/Test/test20/PolyFuns0.bpl index c7d44b9f..b1a4a017 100644 --- a/Test/test20/PolyFuns0.bpl +++ b/Test/test20/PolyFuns0.bpl @@ -1,57 +1,57 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - -function size(x : alpha) returns (int); - -axiom (forall x:int :: size(x) == 0); -axiom (forall x:alpha :: size(x) >= 0); - -axiom (forall m:[int]int, x:int :: size(m) >= m[x]); -axiom (forall m:[a]int :: size(m) == 13); - -type Field a; - -function fieldValue(ref, Field a) returns (a); - -const intField : Field int; -const refField : Field ref; -const obj : ref; -const someInt : int; - -axiom someInt == fieldValue(obj, intField); -axiom someInt == fieldValue(fieldValue(obj, refField), intField); - -axiom someInt == fieldValue(obj, fieldValue(obj, refField)); // error: wrong argument type - -axiom (forall f : Field a :: - (exists x:a :: fieldValue(obj, f) == x)); - -axiom (forall a:alpha, b:beta :: - a == b ==> (exists c:alpha :: c == b)); -axiom (forall f : Field a :: - (exists x:b :: fieldValue(obj, f) == x)); -axiom (forall f : Field a :: - (exists x:int :: fieldValue(obj, f) == x)); - -function lessThan(x : a, y : a) returns (bool); - -axiom (forall x:int, y:int :: x < y ==> lessThan(x, y)); -axiom lessThan(false, true); - -axiom lessThan(5, true); // error: incompatible arguments -axiom (forall x:a, y:b :: lessThan(x, y)); // error: incompatible arguments - -function lessThan2(x : a, y : b) returns (bool); - -axiom (forall x:a, y:a :: lessThan(x,y) == lessThan2(x,y)); -axiom (forall x:a :: (exists m:a :: (forall y:a :: lessThan2(m, y)))); - -axiom (exists x:a, y:b :: lessThan2(x, y) == lessThan2(y, x)); - -axiom (exists x:[Field c]a, y:[Field d]b :: x == y); -axiom (exists x:[Field c]a, y:[Field d]int :: x == y); -axiom (exists x:[Field c]int, y:[Field d]a :: x == y); -axiom (exists x:[Field c]a, y:[Field d]d :: x == y); // error: not unifiable - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +function size(x : alpha) returns (int); + +axiom (forall x:int :: size(x) == 0); +axiom (forall x:alpha :: size(x) >= 0); + +axiom (forall m:[int]int, x:int :: size(m) >= m[x]); +axiom (forall m:[a]int :: size(m) == 13); + +type Field a; + +function fieldValue(ref, Field a) returns (a); + +const intField : Field int; +const refField : Field ref; +const obj : ref; +const someInt : int; + +axiom someInt == fieldValue(obj, intField); +axiom someInt == fieldValue(fieldValue(obj, refField), intField); + +axiom someInt == fieldValue(obj, fieldValue(obj, refField)); // error: wrong argument type + +axiom (forall f : Field a :: + (exists x:a :: fieldValue(obj, f) == x)); + +axiom (forall a:alpha, b:beta :: + a == b ==> (exists c:alpha :: c == b)); +axiom (forall f : Field a :: + (exists x:b :: fieldValue(obj, f) == x)); +axiom (forall f : Field a :: + (exists x:int :: fieldValue(obj, f) == x)); + +function lessThan(x : a, y : a) returns (bool); + +axiom (forall x:int, y:int :: x < y ==> lessThan(x, y)); +axiom lessThan(false, true); + +axiom lessThan(5, true); // error: incompatible arguments +axiom (forall x:a, y:b :: lessThan(x, y)); // error: incompatible arguments + +function lessThan2(x : a, y : b) returns (bool); + +axiom (forall x:a, y:a :: lessThan(x,y) == lessThan2(x,y)); +axiom (forall x:a :: (exists m:a :: (forall y:a :: lessThan2(m, y)))); + +axiom (exists x:a, y:b :: lessThan2(x, y) == lessThan2(y, x)); + +axiom (exists x:[Field c]a, y:[Field d]b :: x == y); +axiom (exists x:[Field c]a, y:[Field d]int :: x == y); +axiom (exists x:[Field c]int, y:[Field d]a :: x == y); +axiom (exists x:[Field c]a, y:[Field d]d :: x == y); // error: not unifiable + +type ref; diff --git a/Test/test20/PolyFuns1.bpl b/Test/test20/PolyFuns1.bpl index 12a8a1b8..01d6638c 100644 --- a/Test/test20/PolyFuns1.bpl +++ b/Test/test20/PolyFuns1.bpl @@ -1,61 +1,61 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -function F( [b]a ) returns (bool); -const M: [ [b]a ] bool; - -procedure P() -{ - var f: [c]c; - var b: bool; - - b := F(f); // type error - b := M[f]; // type error - b := (forall g: [c]c :: F(g)); // type error - b := (forall g: [c]c :: M[g]); // type error -} - -type Field a; -axiom (exists x:[Field c]a, y:[Field d]d :: x == y); // error: not unifiable -axiom (forall x:[Field c]a, y:[Field d]d :: x == y); // error: not unifiable - -procedure Uhu(x: [Field c]a, y: [Field d]d); -procedure Oyeah(t: T) -{ - var xx: [Field cc]T; - var yy:
[Field dd]dd; - var zz: [Field T]ee; - - call Uhu(xx, yy); - call Uhu(yy, yy); // type error in argument 0 - call Uhu(xx, xx); // type error in argument 1 - assert xx == yy; // error: not unifiable - assert yy == xx; // error: not unifiable - - call Uhu(xx, zz); // type error in argument 1 -} - -procedure Jitters() -{ - var x: [a,a]int; - var y: [b,int]int; - var z: [int,c]int; - assert x == y; // error: not unifiable - assert y == z; // error: not unifiable - assert x == z; // error: not unifiable -} - -procedure Nuther() -{ - var x: [a,a,b]int; - var y: [a,b,b]int; - assert x == y; // error: not unifiable -} - -type NagainCtor a; -procedure Nagain() - requires (forall x: a, y: b :: x == y); - ensures (forall x: a, y: Field b, z: NagainCtor b :: x == y && x == z); - ensures (forall y: Field b, z: NagainCtor b :: y == z); // error: types not unifiable -{ -} +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function F( [b]a ) returns (bool); +const M: [ [b]a ] bool; + +procedure P() +{ + var f: [c]c; + var b: bool; + + b := F(f); // type error + b := M[f]; // type error + b := (forall g: [c]c :: F(g)); // type error + b := (forall g: [c]c :: M[g]); // type error +} + +type Field a; +axiom (exists x:[Field c]a, y:[Field d]d :: x == y); // error: not unifiable +axiom (forall x:[Field c]a, y:[Field d]d :: x == y); // error: not unifiable + +procedure Uhu(x: [Field c]a, y: [Field d]d); +procedure Oyeah(t: T) +{ + var xx: [Field cc]T; + var yy:
[Field dd]dd; + var zz: [Field T]ee; + + call Uhu(xx, yy); + call Uhu(yy, yy); // type error in argument 0 + call Uhu(xx, xx); // type error in argument 1 + assert xx == yy; // error: not unifiable + assert yy == xx; // error: not unifiable + + call Uhu(xx, zz); // type error in argument 1 +} + +procedure Jitters() +{ + var x: [a,a]int; + var y: [b,int]int; + var z: [int,c]int; + assert x == y; // error: not unifiable + assert y == z; // error: not unifiable + assert x == z; // error: not unifiable +} + +procedure Nuther() +{ + var x: [a,a,b]int; + var y: [a,b,b]int; + assert x == y; // error: not unifiable +} + +type NagainCtor a; +procedure Nagain() + requires (forall x: a, y: b :: x == y); + ensures (forall x: a, y: Field b, z: NagainCtor b :: x == y && x == z); + ensures (forall y: Field b, z: NagainCtor b :: y == z); // error: types not unifiable +{ +} diff --git a/Test/test20/PolyPolyPoly.bpl b/Test/test20/PolyPolyPoly.bpl index 718452f2..1b2f8823 100644 --- a/Test/test20/PolyPolyPoly.bpl +++ b/Test/test20/PolyPolyPoly.bpl @@ -1,24 +1,24 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type C _; - -const p: []a; -const q: [a, a]a; -const r: [](C a); - -const x: C int; -const y: C bool; - -axiom (p[][:= 5][:= true] == p); -axiom (p[][:= 5][:= true] == r); // error -axiom (p[][:= x][:= y] == p); -axiom (p[][:= x][:= y] == r); -axiom (p[][:= x][:= 5] == r); // error -axiom (p[][:= x][:= y] == p[][:= 5][:= true]); -axiom (q[p[][:= x][:= y], p[][:= 5][:= true]] == p); -axiom (q[p[], p[]][:= 5][:= true] == p); - -axiom (exists x:a :: p[][:= 5][:= true] == x); -axiom (exists x:a, y:b :: p[][:= 5][:= true] == q[x,y]); // error -axiom (exists x:a, y:b :: q[x, x] == q[y, y]); +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type C _; + +const p: []a; +const q: [a, a]a; +const r: [](C a); + +const x: C int; +const y: C bool; + +axiom (p[][:= 5][:= true] == p); +axiom (p[][:= 5][:= true] == r); // error +axiom (p[][:= x][:= y] == p); +axiom (p[][:= x][:= y] == r); +axiom (p[][:= x][:= 5] == r); // error +axiom (p[][:= x][:= y] == p[][:= 5][:= true]); +axiom (q[p[][:= x][:= y], p[][:= 5][:= true]] == p); +axiom (q[p[], p[]][:= 5][:= true] == p); + +axiom (exists x:a :: p[][:= 5][:= true] == x); +axiom (exists x:a, y:b :: p[][:= 5][:= true] == q[x,y]); // error +axiom (exists x:a, y:b :: q[x, x] == q[y, y]); diff --git a/Test/test20/PolyPolyPoly2.bpl b/Test/test20/PolyPolyPoly2.bpl index e50251c1..cf4df9c3 100644 --- a/Test/test20/PolyPolyPoly2.bpl +++ b/Test/test20/PolyPolyPoly2.bpl @@ -1,36 +1,36 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -const p: []a; -const q: [a]b; - -axiom (p[] == p[]); // warning -axiom (p[][13 := false] == q); -axiom (p[][13 := false] == p[]); // warning - -const c: bv17; - -axiom (p[] ++ p[] ++ c == p[]); // warning -axiom (p[] ++ p[] == c); // warning -axiom (p[] == c); - -type List _; - -function emptyList() returns (List a); -function append(List a, List a) returns (List a); - -axiom (forall l:List a :: append(emptyList(), l) == l); -axiom (forall l:List a :: append(l, emptyList()) == l); -axiom (append(emptyList(), emptyList()) == emptyList()); // warning -axiom (forall l:List a :: l==emptyList() ==> append(l, emptyList()) == emptyList()); - -var x: []a; -var y: [a]a; - -procedure P() returns () modifies x, y; { - x[] := 15; - x[] := false; - x[] := p[]; // warning - x[] := q[false]; // warning - y[13] := q[false]; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +const p: []a; +const q: [a]b; + +axiom (p[] == p[]); // warning +axiom (p[][13 := false] == q); +axiom (p[][13 := false] == p[]); // warning + +const c: bv17; + +axiom (p[] ++ p[] ++ c == p[]); // warning +axiom (p[] ++ p[] == c); // warning +axiom (p[] == c); + +type List _; + +function emptyList() returns (List a); +function append(List a, List a) returns (List a); + +axiom (forall l:List a :: append(emptyList(), l) == l); +axiom (forall l:List a :: append(l, emptyList()) == l); +axiom (append(emptyList(), emptyList()) == emptyList()); // warning +axiom (forall l:List a :: l==emptyList() ==> append(l, emptyList()) == emptyList()); + +var x: []a; +var y: [a]a; + +procedure P() returns () modifies x, y; { + x[] := 15; + x[] := false; + x[] := p[]; // warning + x[] := q[false]; // warning + y[13] := q[false]; } \ No newline at end of file diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl index 698e2f12..cc0ba491 100644 --- a/Test/test20/PolyProcs0.bpl +++ b/Test/test20/PolyProcs0.bpl @@ -1,35 +1,35 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - -type Field a; - -function FieldAccessFun(heap : [ref, Field a]a, obj : ref, f : Field b) - returns (res:b); - -procedure FieldAccess(heap : [ref, Field a]a, obj : ref, f : Field b) - returns (res:b) { - start: - res := heap[f, obj]; // error: wrong argument order - res := heap[obj, f]; - assert res == FieldAccessFun(heap, obj, f); - return; -} - -procedure UseHeap(heap : [ref, Field a]a) { - var f1 : Field int; var f2 : Field bool; var obj : ref; - var x : int; var y : bool; - - call x := FieldAccess(heap, f1, obj); // error: wrong argument order - call x := FieldAccess(heap, obj, f1); - call y := FieldAccess(heap, obj, f2); - - call y := FieldAccess(heap, obj, f1); // error: wrong result type - call x := FieldAccess(heap, obj, obj); // error: wrong argument type -} - -procedure injective(heap : [ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b); - requires obj0 != obj1; - ensures heap[obj0, f] != heap[obj1, f]; - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +type Field a; + +function FieldAccessFun(heap : [ref, Field a]a, obj : ref, f : Field b) + returns (res:b); + +procedure FieldAccess(heap : [ref, Field a]a, obj : ref, f : Field b) + returns (res:b) { + start: + res := heap[f, obj]; // error: wrong argument order + res := heap[obj, f]; + assert res == FieldAccessFun(heap, obj, f); + return; +} + +procedure UseHeap(heap : [ref, Field a]a) { + var f1 : Field int; var f2 : Field bool; var obj : ref; + var x : int; var y : bool; + + call x := FieldAccess(heap, f1, obj); // error: wrong argument order + call x := FieldAccess(heap, obj, f1); + call y := FieldAccess(heap, obj, f2); + + call y := FieldAccess(heap, obj, f1); // error: wrong result type + call x := FieldAccess(heap, obj, obj); // error: wrong argument type +} + +procedure injective(heap : [ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b); + requires obj0 != obj1; + ensures heap[obj0, f] != heap[obj1, f]; + +type ref; diff --git a/Test/test20/ProcParamReordering.bpl b/Test/test20/ProcParamReordering.bpl index 2532964f..225eed33 100644 --- a/Test/test20/ProcParamReordering.bpl +++ b/Test/test20/ProcParamReordering.bpl @@ -1,17 +1,17 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type C _; - - -procedure P(x : a, y : b) returns (); - -implementation P(x : a, y : b) returns () {} - -implementation P(a : c, b : d) returns () {} - -implementation P(a : c, b : d) returns () {} - -implementation P(a : c, b : C d) returns () {} - +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type C _; + + +procedure P(x : a, y : b) returns (); + +implementation P(x : a, y : b) returns () {} + +implementation P(a : c, b : d) returns () {} + +implementation P(a : c, b : d) returns () {} + +implementation P(a : c, b : C d) returns () {} + implementation P(x : a, y : a) returns () {} \ No newline at end of file diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl index 26642737..512984dc 100644 --- a/Test/test20/Prog0.bpl +++ b/Test/test20/Prog0.bpl @@ -1,37 +1,37 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// Let's test some Boogie 2 features ... - -type elements; - -type Field a; -var heap : [ref, Field a] a; - -const emptyset : [a] bool; - -function union( [a] bool, [a] bool) returns ( [a] bool); - -axiom (forall x : [a] bool, y : [a] bool, - z : int :: - { union(x, y)[z] } - union(x, y)[z] == (x[z] || y[z])); - -var tau : [ref] int; // error: type variable has to occur in arguments - -axiom (forall x : int :: !emptyset[x]); - -// the more general version of the axiom that also uses type quantifiers - -axiom (forall - x : [a] bool, y : [a] bool, - z : alpha :: - { union(x, y)[z] } - union(x, y)[z] == (x[z] || y[z])); - -axiom (forall a:alpha, b:beta :: // error: variable bound twice - a == b ==> (exists c:alpha :: c == b)); - -axiom (forall a:alpha, b:beta :: // error: alpha is not declared - a == b ==> (exists c:alpha :: c == b)); - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Let's test some Boogie 2 features ... + +type elements; + +type Field a; +var heap : [ref, Field a] a; + +const emptyset : [a] bool; + +function union( [a] bool, [a] bool) returns ( [a] bool); + +axiom (forall x : [a] bool, y : [a] bool, + z : int :: + { union(x, y)[z] } + union(x, y)[z] == (x[z] || y[z])); + +var tau : [ref] int; // error: type variable has to occur in arguments + +axiom (forall x : int :: !emptyset[x]); + +// the more general version of the axiom that also uses type quantifiers + +axiom (forall + x : [a] bool, y : [a] bool, + z : alpha :: + { union(x, y)[z] } + union(x, y)[z] == (x[z] || y[z])); + +axiom (forall a:alpha, b:beta :: // error: variable bound twice + a == b ==> (exists c:alpha :: c == b)); + +axiom (forall a:alpha, b:beta :: // error: alpha is not declared + a == b ==> (exists c:alpha :: c == b)); + +type ref; diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl index 7fcf91b6..1c26db31 100644 --- a/Test/test20/Prog1.bpl +++ b/Test/test20/Prog1.bpl @@ -1,28 +1,28 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// Let's test some Boogie 2 features ... - -type elements; - -type Field a; -var heap : [ref, Field a] a; - - - -procedure p (x:int, y:ref, z: [ref, Field a] a) returns (newHeap : [ref, Field a] a) { - - var f : Field int; - var g : Field bool; - - var heap : [ref, Field a] a; - - assert z[y, f] >= 0; - assert z[x, f] >= 0; // error: x has wrong type - assert z[y, x] >= 0; // error: x has wrong type - assert z[y, g] >= 0; // error: result of map select has wrong type - - heap[y, g] := false; - -} - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Let's test some Boogie 2 features ... + +type elements; + +type Field a; +var heap : [ref, Field a] a; + + + +procedure p (x:int, y:ref, z: [ref, Field a] a) returns (newHeap : [ref, Field a] a) { + + var f : Field int; + var g : Field bool; + + var heap : [ref, Field a] a; + + assert z[y, f] >= 0; + assert z[x, f] >= 0; // error: x has wrong type + assert z[y, x] >= 0; // error: x has wrong type + assert z[y, g] >= 0; // error: result of map select has wrong type + + heap[y, g] := false; + +} + +type ref; diff --git a/Test/test20/Prog2.bpl b/Test/test20/Prog2.bpl index 79555d28..67d9396e 100644 --- a/Test/test20/Prog2.bpl +++ b/Test/test20/Prog2.bpl @@ -1,18 +1,18 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function union( [a] bool, [a] bool) returns ( [a] bool); - -axiom (forall // error: alpha has to occur in dummy types - x : [a] bool, y : [a] bool, - z : int :: - { union(x, y)[z] } - union(x, y)[z] == (x[z] || y[z])); - -function poly() returns (a); - -axiom (forall - x : [a] bool, y : [a] bool, - z : int :: - { union(x, y)[z], poly() : alpha } - union(x, y)[z] == (x[z] || y[z])); - +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function union( [a] bool, [a] bool) returns ( [a] bool); + +axiom (forall // error: alpha has to occur in dummy types + x : [a] bool, y : [a] bool, + z : int :: + { union(x, y)[z] } + union(x, y)[z] == (x[z] || y[z])); + +function poly() returns (a); + +axiom (forall + x : [a] bool, y : [a] bool, + z : int :: + { union(x, y)[z], poly() : alpha } + union(x, y)[z] == (x[z] || y[z])); + diff --git a/Test/test20/TypeDecls0.bpl b/Test/test20/TypeDecls0.bpl index a78008c2..42b988d8 100644 --- a/Test/test20/TypeDecls0.bpl +++ b/Test/test20/TypeDecls0.bpl @@ -1,47 +1,47 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type C a _ b; -type D; -type E _; - -var A0 : D; - -var A1 : C D D D; - -var A2 : [b, C a b D] C a D [D]a; - -var A3 : [b, C a int D] C bool ref [bv32]a; - -var A4 : [a] a; // error: a bound twice -var A5 : [a] [a] int; // error: a bound twice - -var A6 : [a] [b] int; - -var A7 : [a] [int] int; // error: b does not occur as map argument - -type C _ _; // error: C is already declared - -var A8 : C int ref; // error: wrong number of arguments - -var A9 : A0; // error: undeclared type -var A10: F int; // error: undeclared type - -var A11: E D; -var A12: E E D; // error: wrong number of arguments -var A13: E (E D); -var A14: E E E D; // error: wrong number of arguments - -var A15: E E int; // error: wrong number of arguments -var A16: E (E int); - -var A17: bv64; -var A18: [int] bv64; - -var A19: C E E D; // error: wrong number of arguments -var A20: C (E (E D)) int [int] int; -var A21: C ( [a] [b] int) int [int] int; - -var A22: (D); -var A23: ((D)); - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type C a _ b; +type D; +type E _; + +var A0 : D; + +var A1 : C D D D; + +var A2 : [b, C a b D] C a D [D]a; + +var A3 : [b, C a int D] C bool ref [bv32]a; + +var A4 : [a] a; // error: a bound twice +var A5 : [a] [a] int; // error: a bound twice + +var A6 : [a] [b] int; + +var A7 : [a] [int] int; // error: b does not occur as map argument + +type C _ _; // error: C is already declared + +var A8 : C int ref; // error: wrong number of arguments + +var A9 : A0; // error: undeclared type +var A10: F int; // error: undeclared type + +var A11: E D; +var A12: E E D; // error: wrong number of arguments +var A13: E (E D); +var A14: E E E D; // error: wrong number of arguments + +var A15: E E int; // error: wrong number of arguments +var A16: E (E int); + +var A17: bv64; +var A18: [int] bv64; + +var A19: C E E D; // error: wrong number of arguments +var A20: C (E (E D)) int [int] int; +var A21: C ( [a] [b] int) int [int] int; + +var A22: (D); +var A23: ((D)); + +type ref; diff --git a/Test/test20/TypeDecls1.bpl b/Test/test20/TypeDecls1.bpl index 52f28e06..a4fa7de6 100644 --- a/Test/test20/TypeDecls1.bpl +++ b/Test/test20/TypeDecls1.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -// set of maps from anything to a specific type a -const mapSet : [[b]a]bool; - -const emptySet : [a]bool; - -axiom mapSet[5]; // type error - -axiom mapSet[emptySet] == true; - -axiom mapSet[emptySet := false] != mapSet; - -axiom mapSet[emptySet := 5] == mapSet; // type error - -axiom emptySet[13 := true][13] == true; - -axiom (forall f : [c]int, x : ref :: mapSet[f] ==> f[x] >= 0); - -axiom (forall f : [c]c :: mapSet[f]); // type error - -axiom mapSet[mapSet] == true; // type error - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// set of maps from anything to a specific type a +const mapSet : [[b]a]bool; + +const emptySet : [a]bool; + +axiom mapSet[5]; // type error + +axiom mapSet[emptySet] == true; + +axiom mapSet[emptySet := false] != mapSet; + +axiom mapSet[emptySet := 5] == mapSet; // type error + +axiom emptySet[13 := true][13] == true; + +axiom (forall f : [c]int, x : ref :: mapSet[f] ==> f[x] >= 0); + +axiom (forall f : [c]c :: mapSet[f]); // type error + +axiom mapSet[mapSet] == true; // type error + +type ref; diff --git a/Test/test20/TypeSynonyms0.bpl b/Test/test20/TypeSynonyms0.bpl index 1703f4a7..261b94cf 100644 --- a/Test/test20/TypeSynonyms0.bpl +++ b/Test/test20/TypeSynonyms0.bpl @@ -1,33 +1,33 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t" -// RUN: %diff "%s.print.expect" "%t" - - -type Set a = [a]bool; - -type Field a, Heap = [ref, Field a]a; - -type notAllParams a b = Field b; - -type Cyclic0 = Cyclic1; -type Cyclic1 = Cyclic0; - -type AlsoCyclic a = [AlsoCyclic b]int; - -type C a b; - -type C2 b a = C a b; - -function f(C int bool) returns (int); -const x : C2 bool int; - - -const y : Field int bool; // wrong number of arguments -const z : Set int bool; // wrong number of arguments - - -const d : [notAllParams a b]int; // error: not all parameters are used - - -type ref; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t" +// RUN: %diff "%s.print.expect" "%t" + + +type Set a = [a]bool; + +type Field a, Heap = [ref, Field a]a; + +type notAllParams a b = Field b; + +type Cyclic0 = Cyclic1; +type Cyclic1 = Cyclic0; + +type AlsoCyclic a = [AlsoCyclic b]int; + +type C a b; + +type C2 b a = C a b; + +function f(C int bool) returns (int); +const x : C2 bool int; + + +const y : Field int bool; // wrong number of arguments +const z : Set int bool; // wrong number of arguments + + +const d : [notAllParams a b]int; // error: not all parameters are used + + +type ref; diff --git a/Test/test20/TypeSynonyms1.bpl b/Test/test20/TypeSynonyms1.bpl index 98ecedca..9f61335c 100644 --- a/Test/test20/TypeSynonyms1.bpl +++ b/Test/test20/TypeSynonyms1.bpl @@ -1,49 +1,49 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - - -type C a b; -type C2 b a = C a b; - - -// ordering of map type parameters -function g0([C2 a b]int) returns (int); -function g1([C2 b a]int) returns (int); -function g2([C a b]int) returns (int); -function g3([C b a]int) returns (int); - -const c0 : [C2 a b]int; -const c1 : [C2 b a]int; -const c2 : [C a b]int; -const c3 : [C b a]int; - -axiom g0(c0) == 0; -axiom g1(c0) == 0; -axiom g2(c0) == 0; -axiom g3(c0) == 0; -axiom g0(c1) == 0; -axiom g1(c1) == 0; -axiom g2(c1) == 0; -axiom g3(c1) == 0; -axiom g0(c2) == 0; -axiom g1(c2) == 0; -axiom g2(c2) == 0; -axiom g3(c2) == 0; -axiom g0(c3) == 0; -axiom g1(c3) == 0; -axiom g2(c3) == 0; -axiom g3(c3) == 0; - - -type nested a = [b, b, a]int; -type nested2 = nested (nested int); - - -function h(nested2) returns (bool); -const e : [b, b, [b2, b2, int]int]int; -axiom h(e); - -const e2 : [b, b, [b2, b, int]int]int; // wrong binding -axiom h(e2); - +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + + +type C a b; +type C2 b a = C a b; + + +// ordering of map type parameters +function g0([C2 a b]int) returns (int); +function g1([C2 b a]int) returns (int); +function g2([C a b]int) returns (int); +function g3([C b a]int) returns (int); + +const c0 : [C2 a b]int; +const c1 : [C2 b a]int; +const c2 : [C a b]int; +const c3 : [C b a]int; + +axiom g0(c0) == 0; +axiom g1(c0) == 0; +axiom g2(c0) == 0; +axiom g3(c0) == 0; +axiom g0(c1) == 0; +axiom g1(c1) == 0; +axiom g2(c1) == 0; +axiom g3(c1) == 0; +axiom g0(c2) == 0; +axiom g1(c2) == 0; +axiom g2(c2) == 0; +axiom g3(c2) == 0; +axiom g0(c3) == 0; +axiom g1(c3) == 0; +axiom g2(c3) == 0; +axiom g3(c3) == 0; + + +type nested a = [b, b, a]int; +type nested2 = nested (nested int); + + +function h(nested2) returns (bool); +const e : [b, b, [b2, b2, int]int]int; +axiom h(e); + +const e2 : [b, b, [b2, b, int]int]int; // wrong binding +axiom h(e2); + diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl index 1cb6e781..87a7451f 100644 --- a/Test/test20/TypeSynonyms2.bpl +++ b/Test/test20/TypeSynonyms2.bpl @@ -1,24 +1,24 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t" -// RUN: %diff "%s.print.expect" "%t" - - -type Set a = [a]bool; - -function union(x : Set a, y : Set a) returns (Set a); -axiom (forall x : Set a, y : Set a, z : a :: (x[z] || y[z]) == union(x, y)[z]); - - -const intSet0 : Set int; -axiom (forall x:int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); - -const intSet1 : Set int; -axiom (forall x:int :: intSet1[x] == (x == -5 || x == 3)); - - -procedure P() returns () { - assert (forall x:int :: union(intSet0, intSet1)[x] == - (x == -5 || x == 0 || x == 2 || x == 3)); -} - +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t" +// RUN: %diff "%s.print.expect" "%t" + + +type Set a = [a]bool; + +function union(x : Set a, y : Set a) returns (Set a); +axiom (forall x : Set a, y : Set a, z : a :: (x[z] || y[z]) == union(x, y)[z]); + + +const intSet0 : Set int; +axiom (forall x:int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); + +const intSet1 : Set int; +axiom (forall x:int :: intSet1[x] == (x == -5 || x == 3)); + + +procedure P() returns () { + assert (forall x:int :: union(intSet0, intSet1)[x] == + (x == -5 || x == 0 || x == 2 || x == 3)); +} + -- cgit v1.2.3