Test/test1/Frame0.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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;