diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/z3api | |
Initial set of files.
Diffstat (limited to 'Test/z3api')
33 files changed, 1663 insertions, 0 deletions
diff --git a/Test/z3api/Answer b/Test/z3api/Answer new file mode 100644 index 00000000..782aa852 --- /dev/null +++ b/Test/z3api/Answer @@ -0,0 +1,187 @@ +
+-------------------- boog0.bpl --------------------
+boog0.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
+boog0.bpl(45,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog0.bpl(48,7): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- boog1.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog2.bpl --------------------
+boog2.bpl(23,1): Error BP5003: A postcondition might not hold at this return statement.
+boog2.bpl(19,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog2.bpl(22,8): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- boog3.bpl --------------------
+boog3.bpl(6,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog3.bpl(6,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog4.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog5.bpl --------------------
+boog5.bpl(36,3): Error BP5003: A postcondition might not hold at this return statement.
+boog5.bpl(29,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog5.bpl(32,3): anon0
+ boog5.bpl(35,13): anon3_Else
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog7.bpl --------------------
+boog7.bpl(17,1): Error BP5003: A postcondition might not hold at this return statement.
+boog7.bpl(13,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog7.bpl(16,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog8.bpl --------------------
+boog8.bpl(7,12): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
+boog8.bpl(7,18): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
+2 type checking errors detected in boog8.bpl
+
+-------------------- boog9.bpl --------------------
+boog9.bpl(19,1): Error BP5003: A postcondition might not hold at this return statement.
+boog9.bpl(15,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog9.bpl(18,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog10.bpl --------------------
+boog10.bpl(18,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog10.bpl(18,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog11.bpl --------------------
+boog11.bpl(14,1): Error BP5003: A postcondition might not hold at this return statement.
+boog11.bpl(10,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog11.bpl(13,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog12.bpl --------------------
+boog12.bpl(18,1): Error BP5003: A postcondition might not hold at this return statement.
+boog12.bpl(13,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog12.bpl(16,16): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog13.bpl --------------------
+boog13.bpl(9,11): Error: more than one declaration of variable name: v
+1 name resolution errors detected in boog13.bpl
+
+-------------------- boog14.bpl --------------------
+boog14.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.
+boog14.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog14.bpl(10,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog15.bpl --------------------
+boog15.bpl(10,1): Error BP5003: A postcondition might not hold at this return statement.
+boog15.bpl(7,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog15.bpl(9,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog16.bpl --------------------
+boog16.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.
+boog16.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog16.bpl(10,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog17.bpl --------------------
+boog17.bpl(24,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog17.bpl(15,1): start
+ boog17.bpl(19,1): label_3
+ boog17.bpl(22,1): label_4
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog18.bpl --------------------
+boog18.bpl(15,1): Error BP5003: A postcondition might not hold at this return statement.
+boog18.bpl(12,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog18.bpl(14,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog19.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog20.bpl --------------------
+boog20.bpl(15,1): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog20.bpl(15,1): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog21.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog22.bpl --------------------
+boog22.bpl(4,9): Error: more than one declaration of function/procedure name: f1
+1 name resolution errors detected in boog22.bpl
+
+-------------------- boog23.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog24.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog25.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog28.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog29.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog30.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog31.bpl --------------------
+boog31.bpl(12,1): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog31.bpl(12,1): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog34.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/z3api/Boog24.bpl b/Test/z3api/Boog24.bpl new file mode 100644 index 00000000..c5e2eea6 --- /dev/null +++ b/Test/z3api/Boog24.bpl @@ -0,0 +1,16 @@ +
+function LIFT(a:bool) returns (int);
+axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);
+
+procedure main ( )
+
+{
+var a : int;
+var b : int;
+var c : int;
+
+c := LIFT (b < a) ;
+assert (c != 0 <==> b < a);
+
+}
+
diff --git a/Test/z3api/boog0.bpl b/Test/z3api/boog0.bpl new file mode 100644 index 00000000..1b9bee36 --- /dev/null +++ b/Test/z3api/boog0.bpl @@ -0,0 +1,48 @@ +type Wicket;
+const w: Wicket;
+var favorite: Wicket;
+function age(Wicket) returns (int);
+
+axiom age(w)==7;
+
+procedure NewFavorite(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation NewFavorite(l: Wicket) {
+ favorite:=l;
+}
+
+const myBool: bool;
+const myRef: ref;
+const v: Wicket;
+
+axiom 7 < 8;
+axiom 7 <= 8;
+axiom 8 > 7;
+axiom 8 >= 7;
+axiom 6 != 7;
+
+axiom 7+1==8;
+axiom 8-1==7;
+axiom 7/1==7;
+axiom 7%2==1;
+axiom 4*2==8;
+
+axiom ((7==7) || (8==8));
+axiom ((7==7) ==> (7<8));
+axiom ((7==7) <==> (10==10));
+axiom ((7==7) && (8==8));
+
+var favorite2: Wicket;
+procedure SwapFavorites()
+ modifies favorite,favorite2
;
+
+ ensures (favorite==old(favorite2)) && (favorite2==old(favorite));
+{
+ var temp: Wicket;
+ temp:=favorite;
+ favorite:=favorite2;
+ // favorite2:=temp; // commenting this line seeds a bug
+}
diff --git a/Test/z3api/boog1.bpl b/Test/z3api/boog1.bpl new file mode 100644 index 00000000..6b6cce75 --- /dev/null +++ b/Test/z3api/boog1.bpl @@ -0,0 +1,16 @@ +type Wicket;
+const w: Wicket;
+var favorite: Wicket;
+
+function age(Wicket) returns (int);
+
+axiom age(w)==7;
+
+procedure NewFavorite(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation NewFavorite(l: Wicket) {
+ favorite:=l;
+}
\ No newline at end of file diff --git a/Test/z3api/boog10.bpl b/Test/z3api/boog10.bpl new file mode 100644 index 00000000..5ac43287 --- /dev/null +++ b/Test/z3api/boog10.bpl @@ -0,0 +1,22 @@ +// types
+type Color;
+const unique red: Color;
+const unique blue: Color;
+const unique green: Color;
+
+axiom (forall ce:Color :: ce==red || ce==blue || ce==green);
+var myColor: Color;
+
+// procedure
+procedure SetTo(c: Color);
+ modifies myColor
;
+
+ ensures myColor==c;
+
+implementation SetTo(c: Color) {
+ assert (blue==green);
+ myColor:=blue;
+}
+
+
+
diff --git a/Test/z3api/boog11.bpl b/Test/z3api/boog11.bpl new file mode 100644 index 00000000..e66802ea --- /dev/null +++ b/Test/z3api/boog11.bpl @@ -0,0 +1,16 @@ +// types
+const top: ref;
+var myRef: ref;
+
+// procedure
+procedure SetTo(r: ref);
+ modifies myRef
;
+
+ ensures myRef==r;
+
+implementation SetTo(c: ref) {
+ myRef:=top;
+}
+
+
+
diff --git a/Test/z3api/boog12.bpl b/Test/z3api/boog12.bpl new file mode 100644 index 00000000..d20a8f35 --- /dev/null +++ b/Test/z3api/boog12.bpl @@ -0,0 +1,20 @@ +// types
+type Color;
+const blue: Color;
+
+var myArray:[int] Color;
+var myMatrix:[int,int] Color;
+
+// procedure
+procedure SetTo(c: Color);
+ modifies myArray, myMatrix
;
+
+ ensures myArray[0]==c;
+
+implementation SetTo(c: Color) {
+ myMatrix[0,1]:=c;
+ myArray[0]:=blue;
+}
+
+
+
diff --git a/Test/z3api/boog13.bpl b/Test/z3api/boog13.bpl new file mode 100644 index 00000000..a4f854f5 --- /dev/null +++ b/Test/z3api/boog13.bpl @@ -0,0 +1,25 @@ +// types
+type Wicket;
+var favorite: Wicket;
+var v: Wicket;
+
+function age(w:Wicket) returns (int);
+
+axiom (exists v:Wicket :: age(v)<8 &&
+ (forall v:Wicket
:: age(v)==7)
+
+ );
+
+
+// procedure
+procedure SetToSeven(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation SetToSeven(l: Wicket) {
+ favorite:=favorite;
+}
+
+
+
diff --git a/Test/z3api/boog14.bpl b/Test/z3api/boog14.bpl new file mode 100644 index 00000000..c163ed18 --- /dev/null +++ b/Test/z3api/boog14.bpl @@ -0,0 +1,11 @@ +function choose(a:bool, b:int, c:int) returns (x:int);
+axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);
+
+
+var myInt:int;
+procedure main()
+modifies myInt;
+ensures myInt==5;
+{
+ myInt:=4;
+}
\ No newline at end of file diff --git a/Test/z3api/boog15.bpl b/Test/z3api/boog15.bpl new file mode 100644 index 00000000..ef792b2b --- /dev/null +++ b/Test/z3api/boog15.bpl @@ -0,0 +1,10 @@ +function AtLeast(int, int) returns ([int]bool);
+axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
+
+var myInt:int;
+procedure main()
+modifies myInt;
+ensures myInt==5;
+{
+ myInt:=4;
+}
\ No newline at end of file diff --git a/Test/z3api/boog16.bpl b/Test/z3api/boog16.bpl new file mode 100644 index 00000000..48afd41d --- /dev/null +++ b/Test/z3api/boog16.bpl @@ -0,0 +1,11 @@ +function choose(a:bool, b:int, c:int) returns (x:int);
+axiom(forall a:bool, b:int, c:int ::
+ {choose(a,b,c)} !a ==> choose(a,b,c) == c);
+
+var myInt:int;
+procedure main()
+modifies myInt;
+ensures myInt==5;
+{
+ myInt:=4;
+}
\ No newline at end of file diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl new file mode 100644 index 00000000..6f886f49 --- /dev/null +++ b/Test/z3api/boog17.bpl @@ -0,0 +1,25 @@ +const unique g : int;
+axiom(g != 0);
+
+const unique PINT4_name:name;
+
+function PLUS(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
+
+function HasType(v:int, t:name) returns (bool);
+
+
+procedure main ( ) returns ($result.main$11.5$1$:int) {
+ var p : int;
+
+start:
+ assume(HasType(p, PINT4_name));
+ goto label_3;
+
+label_3:
+ goto label_4;
+
+label_4:
+ p := PLUS(g, 4, 55) ;
+ assert(HasType(p, PINT4_name));
+}
\ No newline at end of file diff --git a/Test/z3api/boog18.bpl b/Test/z3api/boog18.bpl new file mode 100644 index 00000000..fe0cbc10 --- /dev/null +++ b/Test/z3api/boog18.bpl @@ -0,0 +1,15 @@ +const A100INT4_name:int;
+
+function Match(a:int, t:int) returns (int);
+function Array(int, int, int) returns (bool);
+
+axiom(forall a:int :: {Match(a, A100INT4_name)} Array(a, 4, 100));
+
+const myNull: int;
+var p: int;
+procedure main()
+modifies p;
+ensures p!=myNull;
+{
+ p:=myNull;
+}
\ No newline at end of file diff --git a/Test/z3api/boog19.bpl b/Test/z3api/boog19.bpl new file mode 100644 index 00000000..17b199dd --- /dev/null +++ b/Test/z3api/boog19.bpl @@ -0,0 +1,228 @@ +var alloc:[int]name;
+
+
+function Field(int) returns (name);
+function Base(int) returns (int);
+
+// Constants
+const unique UNALLOCATED:name;
+const unique ALLOCATED: name;
+const unique FREED:name;
+
+const unique BYTE:name;
+
+function Equal([int]bool, [int]bool) returns (bool);
+function Subset([int]bool, [int]bool) returns (bool);
+function Disjoint([int]bool, [int]bool) returns (bool);
+
+function Empty() returns ([int]bool);
+function Singleton(int) returns ([int]bool);
+function Reachable([int,int]bool, int) returns ([int]bool);
+function Union([int]bool, [int]bool) returns ([int]bool);
+function Intersection([int]bool, [int]bool) returns ([int]bool);
+function Difference([int]bool, [int]bool) returns ([int]bool);
+function Dereference([int]bool, [int]int) returns ([int]bool);
+function Inverse(f:[int]int, x:int) returns ([int]bool);
+
+function AtLeast(int, int) returns ([int]bool);
+function Rep(int, int) returns (int);
+axiom(forall n:int, x:int, y:int :: {AtLeast(n,x)[y]} AtLeast(n,x)[y] ==> x <= y && Rep(n,x) == Rep(n,y));
+axiom(forall n:int, x:int, y:int :: {AtLeast(n,x),Rep(n,x),Rep(n,y)} x <= y && Rep(n,x) == Rep(n,y) ==> AtLeast(n,x)[y]);
+axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
+axiom(forall n:int, x:int, z:int :: {PLUS(x,n,z)} Rep(n,x) == Rep(n,PLUS(x,n,z)));
+axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) - x == n*k));
+
+
+function Array(int, int, int) returns ([int]bool);
+axiom(forall x:int, n:int, z:int :: {Array(x,n,z)} z <= 0 ==> Equal(Array(x,n,z), Empty()));
+axiom(forall x:int, n:int, z:int :: {Array(x,n,z)} z > 0 ==> Equal(Array(x,n,z), Difference(AtLeast(n,x),AtLeast(n,PLUS(x,n,z)))));
+
+
+axiom(forall x:int :: !Empty()[x]);
+
+axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y);
+axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]);
+
+/* this formulation of Union IS more complete than the earlier one */
+/* (A U B)[e], A[d], A U B = Singleton(c), d != e */
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]} Union(S,T)[x] <==> S[x] || T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T), S[x]} S[x] ==> Union(S,T)[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T), T[x]} T[x] ==> Union(S,T)[x]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T)[x]} Intersection(S,T)[x] <==> S[x] && T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T), S[x]} S[x] && T[x] ==> Intersection(S,T)[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T), T[x]} S[x] && T[x] ==> Intersection(S,T)[x]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T)[x]} Difference(S,T)[x] <==> S[x] && !T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T), S[x]} S[x] ==> Difference(S,T)[x] || T[x]);
+
+axiom(forall x:int, S:[int]bool, M:[int]int :: {Dereference(S,M)[x]} Dereference(S,M)[x] ==> (exists y:int :: x == M[y] && S[y]));
+axiom(forall x:int, S:[int]bool, M:[int]int :: {M[x], S[x], Dereference(S,M)} S[x] ==> Dereference(S,M)[M[x]]);
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])} !S[x] ==> Equal(Dereference(S,M[x := y]), Dereference(S,M)));
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])}
+ S[x] && Equal(Intersection(Inverse(M,M[x]), S), Singleton(x)) ==> Equal(Dereference(S,M[x := y]), Union(Difference(Dereference(S,M), Singleton(M[x])), Singleton(y))));
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])}
+ S[x] && !Equal(Intersection(Inverse(M,M[x]), S), Singleton(x)) ==> Equal(Dereference(S,M[x := y]), Union(Dereference(S,M), Singleton(y))));
+
+axiom(forall f:[int]int, x:int :: {Inverse(f,f[x])} Inverse(f,f[x])[x]);
+axiom(forall f:[int]int, x:int, y:int :: {Inverse(f[x := y],y)} Equal(Inverse(f[x := y],y), Union(Inverse(f,y), Singleton(x))));
+axiom(forall f:[int]int, x:int, y:int, z:int :: {Inverse(f[x := y],z)} y == z || Equal(Inverse(f[x := y],z), Difference(Inverse(f,z), Singleton(x))));
+
+axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x], Subset(S,T)} S[x] && Subset(S,T) ==> T[x]);
+axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x]));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x], Disjoint(S,T), T[x]} !(S[x] && Disjoint(S,T) && T[x]));
+axiom(forall S:[int]bool, T:[int]bool :: {Disjoint(S,T)} Disjoint(S,T) || (exists x:int :: S[x] && T[x]));
+
+function Unified([name][int]int) returns ([int]int);
+axiom(forall M:[name][int]int, x:int :: {Unified(M)[x]} Unified(M)[x] == M[Field(x)][x]);
+axiom(forall M:[name][int]int, x:int, y:int :: {Unified(M[Field(x) := M[Field(x)][x := y]])} Unified(M[Field(x) := M[Field(x)][x := y]]) == Unified(M)[x := y]);
+// Memory model
+
+var Mem: [name][int]int;
+
+function Match(a:int, t:name) returns (bool);
+function HasType(v:int, t:name) returns (bool);
+function Values(t:name) returns ([int]bool);
+
+axiom(forall v:int, t:name :: {Values(t)[v]} Values(t)[v] ==> HasType(v, t));
+axiom(forall v:int, t:name :: {HasType(v, t), Values(t)} HasType(v, t) ==> Values(t)[v]);
+
+// Field declarations
+
+
+// Type declarations
+
+const unique A100INT4_name:name;
+const unique INT4_name:name;
+const unique PA100INT4_name:name;
+const unique PINT4_name:name;
+const unique PPINT4_name:name;
+
+// Field definitions
+
+// Type definitions
+
+axiom(forall a:int :: {Match(a, A100INT4_name)} Subset(Empty(), Array(a, 4, 100)));
+axiom(forall a:int, e:int :: {Match(a, A100INT4_name), Array(a, 4, 100)[e]}
+ Match(a, A100INT4_name) && Array(a, 4, 100)[e] ==> Match(e, INT4_name));
+
+axiom(forall a:int :: {Match(a, INT4_name)}
+ Match(a, INT4_name) <==> Field(a) == INT4_name);
+axiom(forall v:int :: HasType(v, INT4_name));
+
+axiom(forall a:int :: {Match(a, PA100INT4_name)}
+ Match(a, PA100INT4_name) <==> Field(a) == PA100INT4_name);
+axiom(forall v:int :: {HasType(v, PA100INT4_name)} {Match(v, A100INT4_name)}
+ HasType(v, PA100INT4_name) <==> (v == 0 || (v > 0 && Match(v, A100INT4_name))));
+
+axiom(forall a:int :: {Match(a, PINT4_name)}
+ Match(a, PINT4_name) <==> Field(a) == PINT4_name);
+axiom(forall v:int :: {HasType(v, PINT4_name)} {Match(v, INT4_name)}
+ HasType(v, PINT4_name) <==> (v == 0 || (v > 0 && Match(v, INT4_name))));
+
+axiom(forall a:int :: {Match(a, PPINT4_name)}
+ Match(a, PPINT4_name) <==> Field(a) == PPINT4_name);
+axiom(forall v:int :: {HasType(v, PPINT4_name)} {Match(v, PINT4_name)}
+ HasType(v, PPINT4_name) <==> (v == 0 || (v > 0 && Match(v, PINT4_name))));
+
+function MINUS_BOTH_PTR_OR_BOTH_INT(a:int, b:int, size:int) returns (int);
+axiom(forall a:int, b:int, size:int :: {MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size)}
+size * MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size) <= a - b && a - b < size * (MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size) + 1));
+
+function MINUS_LEFT_PTR(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {MINUS_LEFT_PTR(a,a_size,b)} MINUS_LEFT_PTR(a,a_size,b) == a - a_size * b);
+
+function PLUS(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
+
+function MULT(a:int, b:int) returns (int); // a*b
+axiom(forall a:int, b:int :: {MULT(a,b)} MULT(a,b) == a * b);
+
+function DIV(a:int, b:int) returns (int); // a/b
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a >= 0 && b > 0 ==> b * DIV(a,b) <= a && a < b * (DIV(a,b) + 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a >= 0 && b < 0 ==> b * DIV(a,b) <= a && a < b * (DIV(a,b) - 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a < 0 && b > 0 ==> b * DIV(a,b) >= a && a > b * (DIV(a,b) - 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a < 0 && b < 0 ==> b * DIV(a,b) >= a && a > b * (DIV(a,b) + 1)
+);
+
+function BINARY_BOTH_INT(a:int, b:int) returns (int);
+/*
+function POW2(a:int) returns (bool);
+axiom POW2(1);
+axiom POW2(2);
+axiom POW2(4);
+axiom POW2(8);
+axiom POW2(16);
+axiom POW2(32);
+axiom POW2(64);
+axiom POW2(128);
+axiom POW2(256);
+axiom POW2(512);
+axiom POW2(1024);
+axiom POW2(2048);
+axiom POW2(4096);
+axiom POW2(8192);
+axiom POW2(16384);
+axiom POW2(32768);
+axiom POW2(65536);
+axiom POW2(131072);
+axiom POW2(262144);
+axiom POW2(524288);
+axiom POW2(1048576);
+axiom POW2(2097152);
+axiom POW2(4194304);
+axiom POW2(8388608);
+axiom POW2(16777216);
+axiom POW2(33554432);
+*/
+function LIFT(a:bool) returns (int);
+axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);
+
+function NOT(a:int) returns (int);
+axiom(forall a:int :: {NOT(a)} a == 0 ==> NOT(a) != 0);
+axiom(forall a:int :: {NOT(a)} a != 0 ==> NOT(a) == 0);
+
+function NULL_CHECK(a:int) returns (int);
+axiom(forall a:int :: {NULL_CHECK(a)} a == 0 ==> NULL_CHECK(a) != 0);
+axiom(forall a:int :: {NULL_CHECK(a)} a != 0 ==> NULL_CHECK(a) == 0);
+
+const unique g : int;
+axiom(g != 0);
+
+
+procedure main ( ) returns ($result.main$11.5$1$:int)
+
+//TAG: requires __objectOf(g) != 0
+requires(Base(g) != 0);
+
+//TAG: requires __allocated(g)
+requires(alloc[Base(g)] == ALLOCATED);
+
+//TAG: requires __allocated(g + 55)
+requires(alloc[Base(PLUS(g, 4, 55))] == ALLOCATED);
+
+//TAG: Type Safety Precondition
+requires(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+requires(HasType(g, PA100INT4_name));
+
+{
+var p : int;
+
+assume(HasType(p, PINT4_name));
+p := PLUS(g, 4, 55) ;
+assert(HasType(p, PINT4_name));
+
+}
+
diff --git a/Test/z3api/boog2.bpl b/Test/z3api/boog2.bpl new file mode 100644 index 00000000..74c05a28 --- /dev/null +++ b/Test/z3api/boog2.bpl @@ -0,0 +1,22 @@ +type Wicket;
+
+var favorite: Wicket;
+var hate: Wicket;
+
+procedure NewFavorite(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation NewFavorite(l: Wicket) {
+ favorite:=l;
+}
+
+
+procedure Swap();
+ modifies favorite,hate;
+ ensures favorite==old(hate);
+
+implementation Swap() {
+ hate := favorite;
+}
\ No newline at end of file diff --git a/Test/z3api/boog20.bpl b/Test/z3api/boog20.bpl new file mode 100644 index 00000000..fa714972 --- /dev/null +++ b/Test/z3api/boog20.bpl @@ -0,0 +1,17 @@ +
+function PLUS(int, int, int) returns (int);
+function Rep(int, int) returns (int);
+
+//PLUS(a,b,z)
+// ERROR
+
+axiom(forall a:int, b:int, z:int :: Rep(a,b) == Rep(a,0));
+axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x));
+// END ERROR
+
+
+procedure main ( )
+{
+assert (PLUS(0, 4, 55)!=0);
+}
+
diff --git a/Test/z3api/boog21.bpl b/Test/z3api/boog21.bpl new file mode 100644 index 00000000..1f4fa6dc --- /dev/null +++ b/Test/z3api/boog21.bpl @@ -0,0 +1,17 @@ +
+function PLUS(int, int, int) returns (int);
+function Rep(int,int) returns (int);
+
+
+// ERROR
+
+axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z
));
+axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x));
+// END ERROR
+
+
+procedure main ( )
+{
+assert (PLUS(0, 4, 55)!=0);
+}
+
diff --git a/Test/z3api/boog22.bpl b/Test/z3api/boog22.bpl new file mode 100644 index 00000000..95e45849 --- /dev/null +++ b/Test/z3api/boog22.bpl @@ -0,0 +1,10 @@ +type W;
+
+function f1(W,int) returns (int);
+function f1(W,int,int) returns (int);
+
+procedure main()
+{
+ var w: W;
+ assert(f1(w,0)==f1(w,0,0));
+}
\ No newline at end of file diff --git a/Test/z3api/boog23.bpl b/Test/z3api/boog23.bpl new file mode 100644 index 00000000..41c68790 --- /dev/null +++ b/Test/z3api/boog23.bpl @@ -0,0 +1,410 @@ +type byte;
+function OneByteToInt(byte) returns (int);
+function TwoBytesToInt(byte, byte) returns (int);
+function FourBytesToInt(byte, byte, byte, byte) returns (int);
+axiom(forall b0:byte, c0:byte :: {OneByteToInt(b0), OneByteToInt(c0)} OneByteToInt(b0) == OneByteToInt(c0) ==> b0 == c0);
+axiom(forall b0:byte, b1: byte, c0:byte, c1:byte :: {TwoBytesToInt(b0, b1), TwoBytesToInt(c0, c1)} TwoBytesToInt(b0, b1) == TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1);
+axiom(forall b0:byte, b1: byte, b2:byte, b3:byte, c0:byte, c1:byte, c2:byte, c3:byte :: {FourBytesToInt(b0, b1, b2, b3), FourBytesToInt(c0, c1, c2, c3)} FourBytesToInt(b0, b1, b2, b3) == FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3);
+
+// Mutable
+var Mem_BYTE:[int]byte;
+var alloc:[int]name;
+
+
+function Field(int) returns (name);
+function Base(int) returns (int);
+
+// Constants
+const unique UNALLOCATED:name;
+const unique ALLOCATED: name;
+const unique FREED:name;
+
+const unique BYTE:name;
+
+function Equal([int]bool, [int]bool) returns (bool);
+function Subset([int]bool, [int]bool) returns (bool);
+function Disjoint([int]bool, [int]bool) returns (bool);
+
+function Empty() returns ([int]bool);
+function Singleton(int) returns ([int]bool);
+function Reachable([int,int]bool, int) returns ([int]bool);
+function Union([int]bool, [int]bool) returns ([int]bool);
+function Intersection([int]bool, [int]bool) returns ([int]bool);
+function Difference([int]bool, [int]bool) returns ([int]bool);
+function Dereference([int]bool, [int]int) returns ([int]bool);
+function Inverse(f:[int]int, x:int) returns ([int]bool);
+
+function AtLeast(int, int) returns ([int]bool);
+function Rep(int, int) returns (int);
+axiom(forall n:int, x:int, y:int :: {AtLeast(n,x)[y]} AtLeast(n,x)[y] ==> x <= y && Rep(n,x) == Rep(n,y));
+axiom(forall n:int, x:int, y:int :: {AtLeast(n,x),Rep(n,x),Rep(n,y)} x <= y && Rep(n,x) == Rep(n,y) ==> AtLeast(n,x)[y]);
+axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
+axiom(forall n:int, x:int, z:int :: {PLUS(x,n,z)} Rep(n,x) == Rep(n,PLUS(x,n,z)));
+axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) - x == n*k));
+
+function Array(int, int, int) returns ([int]bool);
+axiom(forall x:int, n:int, z:int :: {Array(x,n,z)} z <= 0 ==> Equal(Array(x,n,z), Empty()));
+axiom(forall x:int, n:int, z:int :: {Array(x,n,z)} z > 0 ==> Equal(Array(x,n,z), Difference(AtLeast(n,x),AtLeast(n,PLUS(x,n,z)))));
+
+
+axiom(forall x:int :: !Empty()[x]);
+
+axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y);
+axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]);
+
+/* this formulation of Union IS more complete than the earlier one */
+/* (A U B)[e], A[d], A U B = Singleton(c), d != e */
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]} Union(S,T)[x] <==> S[x] || T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T), S[x]} S[x] ==> Union(S,T)[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T), T[x]} T[x] ==> Union(S,T)[x]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T)[x]} Intersection(S,T)[x] <==> S[x] && T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T), S[x]} S[x] && T[x] ==> Intersection(S,T)[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T), T[x]} S[x] && T[x] ==> Intersection(S,T)[x]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T)[x]} Difference(S,T)[x] <==> S[x] && !T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T), S[x]} S[x] ==> Difference(S,T)[x] || T[x]);
+
+axiom(forall x:int, S:[int]bool, M:[int]int :: {Dereference(S,M)[x]} Dereference(S,M)[x] ==> (exists y:int :: x == M[y] && S[y]));
+axiom(forall x:int, S:[int]bool, M:[int]int :: {M[x], S[x], Dereference(S,M)} S[x] ==> Dereference(S,M)[M[x]]);
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])} !S[x] ==> Equal(Dereference(S,M[x := y]), Dereference(S,M)));
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])}
+ S[x] && Equal(Intersection(Inverse(M,M[x]), S), Singleton(x)) ==> Equal(Dereference(S,M[x := y]), Union(Difference(Dereference(S,M), Singleton(M[x])), Singleton(y))));
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])}
+ S[x] && !Equal(Intersection(Inverse(M,M[x]), S), Singleton(x)) ==> Equal(Dereference(S,M[x := y]), Union(Dereference(S,M), Singleton(y))));
+
+axiom(forall f:[int]int, x:int :: {Inverse(f,f[x])} Inverse(f,f[x])[x]);
+axiom(forall f:[int]int, x:int, y:int :: {Inverse(f[x := y],y)} Equal(Inverse(f[x := y],y), Union(Inverse(f,y), Singleton(x))));
+axiom(forall f:[int]int, x:int, y:int, z:int :: {Inverse(f[x := y],z)} y == z || Equal(Inverse(f[x := y],z), Difference(Inverse(f,z), Singleton(x))));
+
+axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x], Subset(S,T)} S[x] && Subset(S,T) ==> T[x]);
+axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x]));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x], Disjoint(S,T), T[x]} !(S[x] && Disjoint(S,T) && T[x]));
+axiom(forall S:[int]bool, T:[int]bool :: {Disjoint(S,T)} Disjoint(S,T) || (exists x:int :: S[x] && T[x]));
+
+function Unified([name][int]int) returns ([int]int);
+axiom(forall M:[name][int]int, x:int :: {Unified(M)[x]} Unified(M)[x] == M[Field(x)][x]);
+axiom(forall M:[name][int]int, x:int, y:int :: {Unified(M[Field(x) := M[Field(x)][x := y]])} Unified(M[Field(x) := M[Field(x)][x := y]]) == Unified(M)[x := y]);
+// Memory model
+
+var Mem: [name][int]int;
+
+function Match(a:int, t:name) returns (bool);
+function HasType(v:int, t:name) returns (bool);
+function Values(t:name) returns ([int]bool);
+
+axiom(forall v:int, t:name :: {Values(t)[v]} Values(t)[v] ==> HasType(v, t));
+axiom(forall v:int, t:name :: {HasType(v, t), Values(t)} HasType(v, t) ==> Values(t)[v]);
+
+// Field declarations
+
+
+// Type declarations
+
+const unique INT4_name:name;
+const unique PINT4_name:name;
+
+// Field definitions
+
+// Type definitions
+
+axiom(forall a:int :: {Match(a, INT4_name)}
+ Match(a, INT4_name) <==> Field(a) == INT4_name);
+axiom(forall v:int :: HasType(v, INT4_name));
+
+axiom(forall a:int :: {Match(a, PINT4_name)}
+ Match(a, PINT4_name) <==> Field(a) == PINT4_name);
+axiom(forall v:int :: {HasType(v, PINT4_name)} {Match(v, INT4_name)}
+ HasType(v, PINT4_name) <==> (v == 0 || (v > 0 && Match(v, INT4_name))));
+
+function MINUS_BOTH_PTR_OR_BOTH_INT(a:int, b:int, size:int) returns (int);
+axiom(forall a:int, b:int, size:int :: {MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size)}
+size * MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size) <= a - b && a - b < size * (MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size) + 1));
+
+function MINUS_LEFT_PTR(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {MINUS_LEFT_PTR(a,a_size,b)} MINUS_LEFT_PTR(a,a_size,b) == a - a_size * b);
+
+function PLUS(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
+
+function MULT(a:int, b:int) returns (int); // a*b
+axiom(forall a:int, b:int :: {MULT(a,b)} MULT(a,b) == a * b);
+
+function DIV(a:int, b:int) returns (int); // a/b
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a >= 0 && b > 0 ==> b * DIV(a,b) <= a && a < b * (DIV(a,b) + 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a >= 0 && b < 0 ==> b * DIV(a,b) <= a && a < b * (DIV(a,b) - 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a < 0 && b > 0 ==> b * DIV(a,b) >= a && a > b * (DIV(a,b) - 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a < 0 && b < 0 ==> b * DIV(a,b) >= a && a > b * (DIV(a,b) + 1)
+);
+
+function BINARY_BOTH_INT(a:int, b:int) returns (int);
+
+function POW2(a:int) returns (bool);
+axiom POW2(1);
+axiom POW2(2);
+axiom POW2(4);
+axiom POW2(8);
+axiom POW2(16);
+axiom POW2(32);
+axiom POW2(64);
+axiom POW2(128);
+axiom POW2(256);
+axiom POW2(512);
+axiom POW2(1024);
+axiom POW2(2048);
+axiom POW2(4096);
+axiom POW2(8192);
+axiom POW2(16384);
+axiom POW2(32768);
+axiom POW2(65536);
+axiom POW2(131072);
+axiom POW2(262144);
+axiom POW2(524288);
+axiom POW2(1048576);
+axiom POW2(2097152);
+axiom POW2(4194304);
+axiom POW2(8388608);
+axiom POW2(16777216);
+axiom POW2(33554432);
+
+function choose(a:bool, b:int, c:int) returns (x:int);
+axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);
+axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} !a ==> choose(a,b,c) == c);
+
+function BIT_BAND(a:int, b:int) returns (x:int);
+axiom(forall a:int, b:int :: {BIT_BAND(a,b)} a == b ==> BIT_BAND(a,b) == a);
+axiom(forall a:int, b:int :: {BIT_BAND(a,b)} POW2(a) && POW2(b) && a != b ==> BIT_BAND(a,b) == 0);
+axiom(forall a:int, b:int :: {BIT_BAND(a,b)} a == 0 || b == 0 ==> BIT_BAND(a,b) == 0);
+
+function BIT_BOR(a:int, b:int) returns (x:int);
+
+function BIT_BXOR(a:int, b:int) returns (x:int);
+
+function BIT_BNOT(a:int) returns (int);
+
+function LIFT(a:bool) returns (int);
+axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);
+
+function NOT(a:int) returns (int);
+axiom(forall a:int :: {NOT(a)} a == 0 ==> NOT(a) != 0);
+axiom(forall a:int :: {NOT(a)} a != 0 ==> NOT(a) == 0);
+
+function NULL_CHECK(a:int) returns (int);
+axiom(forall a:int :: {NULL_CHECK(a)} a == 0 ==> NULL_CHECK(a) != 0);
+axiom(forall a:int :: {NULL_CHECK(a)} a != 0 ==> NULL_CHECK(a) == 0);
+
+procedure nondet_choice() returns (x:int);
+
+
+procedure havoc_assert(i:int);
+requires (i != 0);
+
+procedure havoc_assume(i:int);
+ensures (i != 0);
+
+procedure __HAVOC_free(a:int);
+modifies alloc;
+ensures (forall x:int :: {alloc[x]} x == a || old(alloc)[x] == alloc[x]);
+ensures (alloc[a] == FREED);
+// Additional checks guarded by tranlator flags
+// requires alloc[a] == ALLOCATED;
+// requires Base(a) == a;
+
+procedure __HAVOC_malloc(obj_size:int) returns (new:int);
+requires obj_size >= 0;
+modifies alloc;
+ensures (new > 0);
+ensures (forall x:int :: {Base(x)} new <= x && x < new+obj_size ==> Base(x) == new);
+ensures (forall x:int :: {alloc[x]} x == new || old(alloc)[x] == alloc[x]);
+ensures old(alloc)[new] == UNALLOCATED && alloc[new] == ALLOCATED;
+
+procedure _strdup(str:int) returns (new:int);
+
+procedure _xstrcasecmp(a0:int, a1:int) returns (ret:int);
+
+procedure _xstrcmp(a0:int, a1:int) returns (ret:int);
+
+
+
+
+
+procedure main ( ) returns ($result.main$3.5$1$:int)
+
+modifies alloc;
+//TAG: no freed locations
+ensures(forall f:int :: {alloc[Base(f)]} old(alloc)[Base(f)] == UNALLOCATED || old(alloc)[Base(f)] == alloc[Base(f)]);
+
+modifies Mem;
+//TAG: no updated memory locations
+ensures(forall f: name, m:int :: {Mem[f][m]} Mem[f][m] == old(Mem[f])[m]);
+free ensures(Mem[Field(0)][0] == old(Mem[Field(0)])[0]);
+
+//TAG: Type Safety Precondition
+requires(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+//TAG: Type Safety Postcondition
+ensures(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+ensures(HasType($result.main$3.5$1$, INT4_name));
+{
+var havoc_stringTemp:int;
+var condVal:int;
+var $a$1$4.6$main : int;
+var b : int;
+var c : int;
+var flag : int;
+var tempBoogie0:int;
+var tempBoogie1:int;
+var tempBoogie2:int;
+var tempBoogie3:int;
+var tempBoogie4:int;
+var tempBoogie5:int;
+var tempBoogie6:int;
+var tempBoogie7:int;
+var tempBoogie8:int;
+var tempBoogie9:int;
+var tempBoogie10:int;
+var tempBoogie11:int;
+var tempBoogie12:int;
+var tempBoogie13:int;
+var tempBoogie14:int;
+var tempBoogie15:int;
+var tempBoogie16:int;
+var tempBoogie17:int;
+var tempBoogie18:int;
+var tempBoogie19:int;
+
+
+start:
+
+assume(HasType($a$1$4.6$main, INT4_name));
+assume(HasType(b, INT4_name));
+assume(HasType(c, INT4_name));
+assume(HasType(flag, INT4_name));
+assume(HasType($result.main$3.5$1$, INT4_name));
+goto label_3;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(20)
+label_1:
+assume (forall m:int :: {Mem[Field(m)][m]} alloc[Base(m)] != ALLOCATED && old(alloc)[Base(m)] != ALLOCATED ==> Mem[Field(m)][m] == old(Mem[Field(m)])[m]);
+return;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(20)
+label_2:
+assume false;
+return;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(4)
+label_3:
+goto label_4;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(4)
+label_4:
+goto label_5;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(4)
+label_5:
+goto label_6;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(5)
+label_6:
+goto label_7;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(7)
+label_7:
+c := LIFT(b < $a$1$4.6$main) ;
+//TAG: Type Safety Assertion
+assert(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+assert(HasType($a$1$4.6$main, INT4_name));
+assert(HasType(b, INT4_name));
+assert(HasType(c, INT4_name));
+assert(HasType(flag, INT4_name));
+goto label_8;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(9)
+label_8:
+goto label_8_true , label_8_false ;
+
+
+label_8_true :
+assume (c != 0);
+goto label_10;
+
+
+label_8_false :
+assume (c == 0);
+goto label_9;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(12)
+label_9:
+flag := 0 ;
+//TAG: Type Safety Assertion
+assert(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+assert(HasType($a$1$4.6$main, INT4_name));
+assert(HasType(b, INT4_name));
+assert(HasType(c, INT4_name));
+assert(HasType(flag, INT4_name));
+goto label_11;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(10)
+label_10:
+flag := 1 ;
+//TAG: Type Safety Assertion
+assert(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+assert(HasType($a$1$4.6$main, INT4_name));
+assert(HasType(b, INT4_name));
+assert(HasType(c, INT4_name));
+assert(HasType(flag, INT4_name));
+goto label_11;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(15)
+label_11:
+goto label_11_true , label_11_false ;
+
+
+label_11_true :
+assume (b < $a$1$4.6$main);
+goto label_13;
+
+
+label_11_false :
+assume !(b < $a$1$4.6$main);
+goto label_12;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(18)
+label_12:
+//TAG: flag == 0
+assert (flag == 0);
+goto label_1;
+
+
+// c:\espmain1\esp\tests\hvregr\split_memory\014\bool_vals_gt.c(16)
+label_13:
+//TAG: flag == 1
+assert (flag == 1);
+goto label_1;
+
+}
+
diff --git a/Test/z3api/boog25.bpl b/Test/z3api/boog25.bpl new file mode 100644 index 00000000..0a8b5e92 --- /dev/null +++ b/Test/z3api/boog25.bpl @@ -0,0 +1,282 @@ +type byte;
+function OneByteToInt(byte) returns (int);
+function TwoBytesToInt(byte, byte) returns (int);
+function FourBytesToInt(byte, byte, byte, byte) returns (int);
+axiom(forall b0:byte, c0:byte :: {OneByteToInt(b0), OneByteToInt(c0)} OneByteToInt(b0) == OneByteToInt(c0) ==> b0 == c0);
+axiom(forall b0:byte, b1: byte, c0:byte, c1:byte :: {TwoBytesToInt(b0, b1), TwoBytesToInt(c0, c1)} TwoBytesToInt(b0, b1) == TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1);
+axiom(forall b0:byte, b1: byte, b2:byte, b3:byte, c0:byte, c1:byte, c2:byte, c3:byte :: {FourBytesToInt(b0, b1, b2, b3), FourBytesToInt(c0, c1, c2, c3)} FourBytesToInt(b0, b1, b2, b3) == FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3);
+
+// Mutable
+var Mem_BYTE:[int]byte;
+var alloc:[int]name;
+
+
+function Field(int) returns (name);
+function Base(int) returns (int);
+
+// Constants
+const unique UNALLOCATED:name;
+const unique ALLOCATED: name;
+const unique FREED:name;
+
+const unique BYTE:name;
+
+function Equal([int]bool, [int]bool) returns (bool);
+function Subset([int]bool, [int]bool) returns (bool);
+function Disjoint([int]bool, [int]bool) returns (bool);
+
+function Empty() returns ([int]bool);
+function Singleton(int) returns ([int]bool);
+function Reachable([int,int]bool, int) returns ([int]bool);
+function Union([int]bool, [int]bool) returns ([int]bool);
+function Intersection([int]bool, [int]bool) returns ([int]bool);
+function Difference([int]bool, [int]bool) returns ([int]bool);
+function Dereference([int]bool, [int]int) returns ([int]bool);
+function Inverse(f:[int]int, x:int) returns ([int]bool);
+
+function AtLeast(int, int) returns ([int]bool);
+function Rep(int, int) returns (int);
+axiom(forall n:int, x:int, y:int :: {AtLeast(n,x)[y]} AtLeast(n,x)[y] ==> x <= y && Rep(n,x) == Rep(n,y));
+axiom(forall n:int, x:int, y:int :: {AtLeast(n,x),Rep(n,x),Rep(n,y)} x <= y && Rep(n,x) == Rep(n,y) ==> AtLeast(n,x)[y]);
+axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
+axiom(forall n:int, x:int, z:int :: {PLUS(x,n,z)} Rep(n,x) == Rep(n,PLUS(x,n,z)));
+axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) - x == n*k));
+
+/*
+function AtLeast(int, int) returns ([int]bool);
+function ModEqual(int, int, int) returns (bool);
+axiom(forall n:int, x:int :: ModEqual(n,x,x));
+axiom(forall n:int, x:int, y:int :: {ModEqual(n,x,y)} ModEqual(n,x,y) ==> ModEqual(n,y,x));
+axiom(forall n:int, x:int, y:int, z:int :: {ModEqual(n,x,y), ModEqual(n,y,z)} ModEqual(n,x,y) && ModEqual(n,y,z) ==> ModEqual(n,x,z));
+axiom(forall n:int, x:int, z:int :: {PLUS(x,n,z)} ModEqual(n,x,PLUS(x,n,z)));
+axiom(forall n:int, x:int, y:int :: {ModEqual(n,x,y)} ModEqual(n,x,y) ==> (exists k:int :: x - y == n*k));
+axiom(forall x:int, n:int, y:int :: {AtLeast(n,x)[y]}{ModEqual(n,x,y)} AtLeast(n,x)[y] <==> x <= y && ModEqual(n,x,y));
+axiom(forall x:int, n:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
+*/
+
+function Array(int, int, int) returns ([int]bool);
+axiom(forall x:int, n:int, z:int :: {Array(x,n,z)} z <= 0 ==> Equal(Array(x,n,z), Empty()));
+axiom(forall x:int, n:int, z:int :: {Array(x,n,z)} z > 0 ==> Equal(Array(x,n,z), Difference(AtLeast(n,x),AtLeast(n,PLUS(x,n,z)))));
+
+
+axiom(forall x:int :: !Empty()[x]);
+
+axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y);
+axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]);
+
+/* this formulation of Union IS more complete than the earlier one */
+/* (A U B)[e], A[d], A U B = Singleton(c), d != e */
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]} Union(S,T)[x] <==> S[x] || T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T), S[x]} S[x] ==> Union(S,T)[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T), T[x]} T[x] ==> Union(S,T)[x]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T)[x]} Intersection(S,T)[x] <==> S[x] && T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T), S[x]} S[x] && T[x] ==> Intersection(S,T)[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T), T[x]} S[x] && T[x] ==> Intersection(S,T)[x]);
+
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T)[x]} Difference(S,T)[x] <==> S[x] && !T[x]);
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T), S[x]} S[x] ==> Difference(S,T)[x] || T[x]);
+
+axiom(forall x:int, S:[int]bool, M:[int]int :: {Dereference(S,M)[x]} Dereference(S,M)[x] ==> (exists y:int :: x == M[y] && S[y]));
+axiom(forall x:int, S:[int]bool, M:[int]int :: {M[x], S[x], Dereference(S,M)} S[x] ==> Dereference(S,M)[M[x]]);
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])} !S[x] ==> Equal(Dereference(S,M[x := y]), Dereference(S,M)));
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])}
+ S[x] && Equal(Intersection(Inverse(M,M[x]), S), Singleton(x)) ==> Equal(Dereference(S,M[x := y]), Union(Difference(Dereference(S,M), Singleton(M[x])), Singleton(y))));
+axiom(forall x:int, y:int, S:[int]bool, M:[int]int :: {Dereference(S,M[x := y])}
+ S[x] && !Equal(Intersection(Inverse(M,M[x]), S), Singleton(x)) ==> Equal(Dereference(S,M[x := y]), Union(Dereference(S,M), Singleton(y))));
+
+axiom(forall f:[int]int, x:int :: {Inverse(f,f[x])} Inverse(f,f[x])[x]);
+axiom(forall f:[int]int, x:int, y:int :: {Inverse(f[x := y],y)} Equal(Inverse(f[x := y],y), Union(Inverse(f,y), Singleton(x))));
+axiom(forall f:[int]int, x:int, y:int, z:int :: {Inverse(f[x := y],z)} y == z || Equal(Inverse(f[x := y],z), Difference(Inverse(f,z), Singleton(x))));
+
+axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x], Subset(S,T)} S[x] && Subset(S,T) ==> T[x]);
+axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x]));
+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x], Disjoint(S,T), T[x]} !(S[x] && Disjoint(S,T) && T[x]));
+axiom(forall S:[int]bool, T:[int]bool :: {Disjoint(S,T)} Disjoint(S,T) || (exists x:int :: S[x] && T[x]));
+
+function Unified([name][int]int) returns ([int]int);
+axiom(forall M:[name][int]int, x:int :: {Unified(M)[x]} Unified(M)[x] == M[Field(x)][x]);
+axiom(forall M:[name][int]int, x:int, y:int :: {Unified(M[Field(x) := M[Field(x)][x := y]])} Unified(M[Field(x) := M[Field(x)][x := y]]) == Unified(M)[x := y]);
+// Memory model
+
+var Mem: [name][int]int;
+
+function Match(a:int, t:name) returns (bool);
+function HasType(v:int, t:name) returns (bool);
+function Values(t:name) returns ([int]bool);
+
+axiom(forall v:int, t:name :: {Values(t)[v]} Values(t)[v] ==> HasType(v, t));
+axiom(forall v:int, t:name :: {HasType(v, t), Values(t)} HasType(v, t) ==> Values(t)[v]);
+
+// Field declarations
+
+
+// Type declarations
+
+const unique INT4_name:name;
+const unique PINT4_name:name;
+
+// Field definitions
+
+// Type definitions
+
+axiom(forall a:int :: {Match(a, INT4_name)}
+ Match(a, INT4_name) <==> Field(a) == INT4_name);
+axiom(forall v:int :: HasType(v, INT4_name));
+
+axiom(forall a:int :: {Match(a, PINT4_name)}
+ Match(a, PINT4_name) <==> Field(a) == PINT4_name);
+axiom(forall v:int :: {HasType(v, PINT4_name)} {Match(v, INT4_name)}
+ HasType(v, PINT4_name) <==> (v == 0 || (v > 0 && Match(v, INT4_name))));
+
+function MINUS_BOTH_PTR_OR_BOTH_INT(a:int, b:int, size:int) returns (int);
+axiom(forall a:int, b:int, size:int :: {MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size)}
+size * MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size) <= a - b && a - b < size * (MINUS_BOTH_PTR_OR_BOTH_INT(a,b,size) + 1));
+
+function MINUS_LEFT_PTR(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {MINUS_LEFT_PTR(a,a_size,b)} MINUS_LEFT_PTR(a,a_size,b) == a - a_size * b);
+
+function PLUS(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
+
+function MULT(a:int, b:int) returns (int); // a*b
+axiom(forall a:int, b:int :: {MULT(a,b)} MULT(a,b) == a * b);
+
+function DIV(a:int, b:int) returns (int); // a/b
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a >= 0 && b > 0 ==> b * DIV(a,b) <= a && a < b * (DIV(a,b) + 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a >= 0 && b < 0 ==> b * DIV(a,b) <= a && a < b * (DIV(a,b) - 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a < 0 && b > 0 ==> b * DIV(a,b) >= a && a > b * (DIV(a,b) - 1)
+);
+
+axiom(forall a:int, b:int :: {DIV(a,b)}
+a < 0 && b < 0 ==> b * DIV(a,b) >= a && a > b * (DIV(a,b) + 1)
+);
+
+function BINARY_BOTH_INT(a:int, b:int) returns (int);
+
+function POW2(a:int) returns (bool);
+axiom POW2(1);
+axiom POW2(2);
+axiom POW2(4);
+axiom POW2(8);
+axiom POW2(16);
+axiom POW2(32);
+axiom POW2(64);
+axiom POW2(128);
+axiom POW2(256);
+axiom POW2(512);
+axiom POW2(1024);
+axiom POW2(2048);
+axiom POW2(4096);
+axiom POW2(8192);
+axiom POW2(16384);
+axiom POW2(32768);
+axiom POW2(65536);
+axiom POW2(131072);
+axiom POW2(262144);
+axiom POW2(524288);
+axiom POW2(1048576);
+axiom POW2(2097152);
+axiom POW2(4194304);
+axiom POW2(8388608);
+axiom POW2(16777216);
+axiom POW2(33554432);
+
+function choose(a:bool, b:int, c:int) returns (x:int);
+axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);
+axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} !a ==> choose(a,b,c) == c);
+
+function BIT_BAND(a:int, b:int) returns (x:int);
+axiom(forall a:int, b:int :: {BIT_BAND(a,b)} a == b ==> BIT_BAND(a,b) == a);
+axiom(forall a:int, b:int :: {BIT_BAND(a,b)} POW2(a) && POW2(b) && a != b ==> BIT_BAND(a,b) == 0);
+axiom(forall a:int, b:int :: {BIT_BAND(a,b)} a == 0 || b == 0 ==> BIT_BAND(a,b) == 0);
+
+function BIT_BOR(a:int, b:int) returns (x:int);
+
+function BIT_BXOR(a:int, b:int) returns (x:int);
+
+function BIT_BNOT(a:int) returns (int);
+
+function LIFT(a:bool) returns (int);
+axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);
+
+function NOT(a:int) returns (int);
+axiom(forall a:int :: {NOT(a)} a == 0 ==> NOT(a) != 0);
+axiom(forall a:int :: {NOT(a)} a != 0 ==> NOT(a) == 0);
+
+function NULL_CHECK(a:int) returns (int);
+axiom(forall a:int :: {NULL_CHECK(a)} a == 0 ==> NULL_CHECK(a) != 0);
+axiom(forall a:int :: {NULL_CHECK(a)} a != 0 ==> NULL_CHECK(a) == 0);
+
+procedure nondet_choice() returns (x:int);
+
+
+procedure havoc_assert(i:int);
+requires (i != 0);
+
+procedure havoc_assume(i:int);
+ensures (i != 0);
+
+procedure __HAVOC_free(a:int);
+modifies alloc;
+ensures (forall x:int :: {alloc[x]} x == a || old(alloc)[x] == alloc[x]);
+ensures (alloc[a] == FREED);
+// Additional checks guarded by tranlator flags
+// requires alloc[a] == ALLOCATED;
+// requires Base(a) == a;
+
+procedure __HAVOC_malloc(obj_size:int) returns (new:int);
+requires obj_size >= 0;
+modifies alloc;
+ensures (new > 0);
+ensures (forall x:int :: {Base(x)} new <= x && x < new+obj_size ==> Base(x) == new);
+ensures (forall x:int :: {alloc[x]} x == new || old(alloc)[x] == alloc[x]);
+ensures old(alloc)[new] == UNALLOCATED && alloc[new] == ALLOCATED;
+
+procedure _strdup(str:int) returns (new:int);
+
+procedure _xstrcasecmp(a0:int, a1:int) returns (ret:int);
+
+procedure _xstrcmp(a0:int, a1:int) returns (ret:int);
+
+
+
+
+
+procedure main ( ) returns ($result.main$3.5$1$:int)
+
+modifies alloc;
+//TAG: no freed locations
+ensures(forall f:int :: {alloc[Base(f)]} old(alloc)[Base(f)] == UNALLOCATED || old(alloc)[Base(f)] == alloc[Base(f)]);
+
+modifies Mem;
+//TAG: no updated memory locations
+ensures(forall f: name, m:int :: {Mem[f][m]} Mem[f][m] == old(Mem[f])[m]);
+free ensures(Mem[Field(0)][0] == old(Mem[Field(0)])[0]);
+
+//TAG: Type Safety Precondition
+requires(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+//TAG: Type Safety Postcondition
+ensures(forall a:int :: {Mem[Field(a)][a]} HasType(Mem[Field(a)][a], Field(a)));
+ensures(HasType($result.main$3.5$1$, INT4_name));
+{
+
+var a : int;
+var b : int;
+var c : int;
+
+c := LIFT (b < a) ;
+assert (c != 0 <==> b < a);
+
+
+}
+
diff --git a/Test/z3api/boog28.bpl b/Test/z3api/boog28.bpl new file mode 100644 index 00000000..989dbf75 --- /dev/null +++ b/Test/z3api/boog28.bpl @@ -0,0 +1,16 @@ +
+function LIFT(x:bool) returns (int);
+axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
+
+procedure main ( )
+
+{
+var a : int;
+var b : int;
+var c : int;
+
+c := LIFT (b == a) ;
+assert (c != 0 <==> b == a);
+
+}
+
diff --git a/Test/z3api/boog29.bpl b/Test/z3api/boog29.bpl new file mode 100644 index 00000000..8a97944d --- /dev/null +++ b/Test/z3api/boog29.bpl @@ -0,0 +1,19 @@ +
+function LIFT(x:bool) returns (int);
+axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
+
+procedure main ( )
+
+{
+var c: int;
+c := LIFT(false);
+assert (c==0);
+
+c := LIFT(true);
+assert (c!=0);
+/*
+c := LIFT(1==5);
+assert (c==0);
+*/
+}
+
diff --git a/Test/z3api/boog3.bpl b/Test/z3api/boog3.bpl new file mode 100644 index 00000000..9e04ac5b --- /dev/null +++ b/Test/z3api/boog3.bpl @@ -0,0 +1,7 @@ +type Wicket;
+
+procedure Dummy();
+implementation Dummy() {
+ var x: Wicket;
+ assert (x!=x);
+}
\ No newline at end of file diff --git a/Test/z3api/boog30.bpl b/Test/z3api/boog30.bpl new file mode 100644 index 00000000..ae682156 --- /dev/null +++ b/Test/z3api/boog30.bpl @@ -0,0 +1,13 @@ +
+function LIFT(x:bool) returns (int);
+axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
+
+procedure main ( )
+
+{
+var c: int;
+
+c := LIFT(1==5);
+assert (c==0);
+}
+
diff --git a/Test/z3api/boog31.bpl b/Test/z3api/boog31.bpl new file mode 100644 index 00000000..219effce --- /dev/null +++ b/Test/z3api/boog31.bpl @@ -0,0 +1,14 @@ +
+const b1:bool;
+const b2:bool;
+const b3:bool;
+
+axiom (b1==true && b2==false && b3==true);
+
+procedure main ( )
+
+{
+var c: int;
+assert (c==0);
+}
+
diff --git a/Test/z3api/boog34.bpl b/Test/z3api/boog34.bpl new file mode 100644 index 00000000..62e7e82b --- /dev/null +++ b/Test/z3api/boog34.bpl @@ -0,0 +1,10 @@ +
+function Rep(int, int) returns (int);
+axiom(forall n:int, x:int :: {Rep(n,x)}
+ (exists k:int :: Rep(n,x) - x == n*k));
+
+procedure main(x:int)
+{
+assert((Rep(0,x)==x));
+return;
+}
\ No newline at end of file diff --git a/Test/z3api/boog4.bpl b/Test/z3api/boog4.bpl new file mode 100644 index 00000000..46eda549 --- /dev/null +++ b/Test/z3api/boog4.bpl @@ -0,0 +1,40 @@ +type Wicket;
+
+const w: Wicket;
+const myBool: bool;
+const v: Wicket;
+
+var favorite: Wicket;
+
+function age(Wicket) returns (int);
+
+axiom age(w)==7;
+axiom 7 < 8;
+axiom 7 <= 8;
+axiom 8 > 7;
+axiom 8 >= 7;
+axiom 6 != 7;
+axiom 7+1==8;
+axiom 8-1==7;
+axiom 7/1==7;
+axiom 7%2==1;
+axiom 4*2==8;
+axiom ((7==7) || (8==8));
+axiom ((7==7) ==> (7<8));
+axiom ((7==7) <==> (10==10));
+axiom ((7==7) && (8==8));
+
+axiom 7!=7;
+
+
+procedure NewFavorite(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation NewFavorite(l: Wicket) {
+ favorite:=l;
+}
+
+
+
diff --git a/Test/z3api/boog5.bpl b/Test/z3api/boog5.bpl new file mode 100644 index 00000000..0db94bba --- /dev/null +++ b/Test/z3api/boog5.bpl @@ -0,0 +1,40 @@ +// types
+type Wicket;
+
+// consts
+const w: Wicket;
+const myBool: bool;
+const v: Wicket;
+const u: Wicket;
+const x: Wicket;
+
+
+// vars
+var favorite: Wicket;
+
+// functions
+function age(Wicket) returns (int);
+
+// axioms
+axiom age(w)==6;
+axiom age(u)==5;
+axiom age(x)==4;
+
+
+// procedure
+procedure SetToSeven(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation SetToSeven(l: Wicket) {
+ if (age(w)==7) {
+ favorite:=l;
+ } else {
+ favorite:=v;
+ }
+
+}
+
+
+
diff --git a/Test/z3api/boog6.bpl b/Test/z3api/boog6.bpl new file mode 100644 index 00000000..55c1dc7e --- /dev/null +++ b/Test/z3api/boog6.bpl @@ -0,0 +1,22 @@ +// types
+type Wicket;
+
+// consts
+var favorite: Wicket;
+
+// axioms
+const b: bool;
+axiom b==true;
+
+// procedure
+procedure SetToSeven(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation SetToSeven(l: Wicket) {
+ favorite:=l;
+}
+
+
+
diff --git a/Test/z3api/boog7.bpl b/Test/z3api/boog7.bpl new file mode 100644 index 00000000..36f952d1 --- /dev/null +++ b/Test/z3api/boog7.bpl @@ -0,0 +1,19 @@ +// consts
+const w: int;
+
+
+// vars
+var favorite: int;
+
+// procedure
+procedure SetToSeven(p: int);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation SetToSeven(l: int) {
+ favorite:=w;
+}
+
+
+
diff --git a/Test/z3api/boog8.bpl b/Test/z3api/boog8.bpl new file mode 100644 index 00000000..0ac4f163 --- /dev/null +++ b/Test/z3api/boog8.bpl @@ -0,0 +1,24 @@ +// types
+type Wicket;
+var favorite: Wicket;
+
+
+const myBv: bv5;
+axiom myBv==1bv2++2bv3;
+
+const myBool: bool;
+axiom myBool==true;
+
+
+// procedure
+procedure SetToSeven(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation SetToSeven(l: Wicket) {
+ favorite:=favorite;
+}
+
+
+
diff --git a/Test/z3api/boog9.bpl b/Test/z3api/boog9.bpl new file mode 100644 index 00000000..55897a1d --- /dev/null +++ b/Test/z3api/boog9.bpl @@ -0,0 +1,21 @@ +// types
+type Wicket;
+var favorite: Wicket;
+
+function age(w:Wicket) returns (int);
+axiom (forall v:Wicket :: age(v)==7);
+axiom (exists v:Wicket :: age(v)<8);
+
+
+// procedure
+procedure SetToSeven(p: Wicket);
+ modifies favorite
;
+
+ ensures favorite==p;
+
+implementation SetToSeven(l: Wicket) {
+ favorite:=favorite;
+}
+
+
+
diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat new file mode 100644 index 00000000..5daa36c0 --- /dev/null +++ b/Test/z3api/runtest.bat @@ -0,0 +1,10 @@ +@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /prover:z3api %%f
+)
|