summaryrefslogtreecommitdiff
path: root/Test/test20/ParallelAssignment.bpl
blob: b79d1a10f5aa3bed424ca74c39138061936de133 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
// RUN: %boogie -noVerify %s > %t
// RUN: %diff %s.expect %t
// Examples from the Boogie2 language report
// (stuff where resolution succeeds, but typechecking might fail)

type C, D;

var x : int;
var y : int;
var z : int;
var a : [int]int;
var b : [int][C, D]int;

procedure P(i:int, j:int, m:C, n:D) returns () modifies x, y, a, b; {
  x := x+1;
  a[i] := 12;
  x, y := y, x;
  x, a[i] := x+1, x;
  x := true;            // type error
  a[true] := 5;         // type error

  z := 23;              // assignment to non-modifiable variable
  b[i][m, n] := 17;
  b[i][m, n], x := a[x], y;
}