blob: 4e031cb81c48cf51deeba14c56e5dd0e526998f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"
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;
// CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
Q[5,8] := q;
// not like this:
// CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
Q[5,8][13] := 21; // error: the updated array must be an identifier
return;
}
// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME}
|