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/Frame1.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test1/Frame1.bpl')
| -rw-r--r-- | Test/test1/Frame1.bpl | 97 |
1 files changed, 97 insertions, 0 deletions
diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl new file mode 100644 index 00000000..469f43ba --- /dev/null +++ b/Test/test1/Frame1.bpl @@ -0,0 +1,97 @@ +var g0: int;
+var g1: int;
+
+var h0: [ref, name]int;
+var h1: [ref, name]int;
+
+const X: name;
+
+procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
+ modifies h1, g0;
+
+implementation P(a: ref, hh: [ref, name]int)
+ returns (b: int, hout: [ref, name]any) {
+ start:
+ g0 := 5;
+ g1 := 6; // error: g1 is not in modifies clause
+ a := null; // error: in-parameters are not mutable
+ b := 12;
+ goto next;
+ next:
+ havoc g0;
+ havoc g1; // error: g1 is not in modifies clause
+ havoc a; // error: in-parameters are not mutable
+ havoc b;
+ goto more;
+ more:
+ hh[a,X] := 101; // error: in-parameter (hh) is not mutable
+ h0[a,X] := 102; // error: h0 is not in modifies clause
+ h1[a,X] := 103;
+ hh := h0; // error: in-parameter is not mutable
+ h0 := h1; // error: h0 is not in modifies clause
+ h1 := hh;
+ havoc hh; // error: in-parameter is not mutable
+ havoc h0; // error: h0 is not in modifies clause
+ havoc h1;
+ return;
+}
+
+procedure PX();
+ modifies h1, g0;
+
+procedure PY()
+ modifies h1, g0;
+{
+ start:
+ call PX();
+ call PY();
+ return;
+}
+
+procedure PZ()
+ modifies h1;
+{
+ start:
+ call PX(); // error: PX has larger frame than PZ
+ return;
+}
+
+procedure Q() returns (x: int, y: int, h: [ref, name]int)
+{
+ start:
+ return;
+}
+
+procedure QCallerBad()
+{
+ start:
+ call g0, g1, h0 := Q();
+ return;
+}
+
+procedure QCallerGood()
+ modifies g0, h0;
+{
+ var t: int;
+
+ start:
+ call t, g0, h0 := Q();
+ return;
+}
+
+procedure MismatchedTypes(x: int);
+
+implementation MismatchedTypes(x: bool) // error
+{
+ start:
+ return;
+}
+implementation MismatchedTypes(y: bool) // error (this time with a different name for the formal)
+{
+ start:
+ return;
+}
+
+
+type ref, name, any;
+const null : ref;
|