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/test1/MapsTypeErrors.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test1/MapsTypeErrors.bpl')
| -rw-r--r-- | Test/test1/MapsTypeErrors.bpl | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/Test/test1/MapsTypeErrors.bpl b/Test/test1/MapsTypeErrors.bpl new file mode 100644 index 00000000..0e68440d --- /dev/null +++ b/Test/test1/MapsTypeErrors.bpl @@ -0,0 +1,127 @@ +var m: []int;
+var p: <a>[]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<T>(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 = <a>[ref, Field a]a;
+const F0: Field int;
+const F1: Field bool;
+const alloc: Field bool;
+var Heap: HeapType;
+
+function LiberalEqual<a,b>(a, b) returns (bool);
+function StrictEqual<a>(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<alpha> 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<T>() returns (T);
+function Same<T>(T,T) returns (T);
+procedure ConsumeAnything<T>(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];
+}
|