//# publish module 0x1.M { import 0x1.vector; struct R has key { v: vector } public publish(s: &signer) { label b0: move_to(move(s), R { v: vector.empty() }); return; } public borrow_and_push(addr: address) acquires R { let r: &mut Self.R; label b0: r = borrow_global_mut(move(addr)); vector.push_back(&mut move(r).R::v, 42); return; } public verify_effects(addr: address) acquires R { let r: &Self.R; label b0: r = borrow_global(move(addr)); assert(vector.length(& move(r).R::v) == 1, 1000); return; } } //# run --signers 0x1 import 0x1.M; main(s: signer) { label b0: M.publish(&s); return; } //# run --signers 0x1 import 0x1.M; import 0x1.signer; main(s: signer) { label b0: M.borrow_and_push(signer.address_of(&s)); return; } //# run --signers 0x1 import 0x1.M; import 0x1.signer; main(s: signer) { label b0: M.verify_effects(signer.address_of(&s)); return; }