blob: 6155fc27150049ba04b64e277163b3c8646533d4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
var g0: int;
var g1: int;
var h0: [ref, name]any;
var h1: [ref, name]any;
const X: name;
procedure P(a: ref, hh: [ref, name]any) returns (b: int, hout: [ref, name]any);
modifies a; // in-parameters are not mutable
modifies h1, g0;
modifies b; // out-parameters are not allowed explicitly in modifies clause
type ref, name, any;
|
