summaryrefslogtreecommitdiff
path: root/Test/z3api/boog12.bpl
blob: c277a6744dbf46d0ad657049713e9a34caab0a33 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
type ref;
// types
type Color;
const blue: Color;

var myArray:[int] Color;
var myMatrix:[int,int] Color;

// procedure
procedure SetTo(c: Color);
  modifies myArray, myMatrix
;

  ensures myArray[0]==c;

implementation SetTo(c: Color) {
  myMatrix[0,1]:=c;
  myArray[0]:=blue;
}