Skip to content

Commit 2fb2da2

Browse files
committed
Create multi_initialization.vpr
1 parent b149ceb commit 2fb2da2

1 file changed

Lines changed: 17 additions & 0 deletions

File tree

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// Any copyright is dedicated to the Public Domain.
2+
// http://creativecommons.org/publicdomain/zero/1.0/
3+
4+
field n: Ref
5+
6+
method get_refs() returns (x: Ref, y: Ref)
7+
ensures acc(x.n)
8+
9+
method foo() {
10+
var a: Ref, b: Ref
11+
12+
var c: Ref, d: Ref := get_refs()
13+
var e: Ref := new(n)
14+
15+
c.n, e := get_refs()
16+
c.n.n := new(n)
17+
}

0 commit comments

Comments
 (0)