diff options
Diffstat (limited to 'Test/test0/Arrays1.bpl')
| -rw-r--r-- | Test/test0/Arrays1.bpl | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl new file mode 100644 index 00000000..db12ecb3 --- /dev/null +++ b/Test/test0/Arrays1.bpl @@ -0,0 +1,16 @@ +var Q: [int,int][int]int;
+
+procedure P()
+{
+ var q: [int]int;
+
+ start:
+ // here's how to do it:
+ q := Q[5,8];
+ q[13] := 21;
+ Q[5,8] := q;
+
+ // not like this:
+ Q[5,8][13] := 21; // error: the updated array must be an identifier
+ return;
+}
|