blob: 0e36bcdd8dc0baa9dca311dc210283f34c662664 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// RUN: %boogie -noVerify %s > %t
// RUN: %diff %s.expect %t
// Examples from the Boogie2 language report
// (examples where already resolution fails)
var x : int;
var y : int;
var a : [int]int;
procedure P(i:int, j:int) returns () modifies x, y, a; {
x, y := 1; // wrong number of rhss
a[i], a[j] := a[j], a[i]; // variable assigned more than once
}
|
