// flag: --v2 address 0x0 { /// Example for opaque function calls with `modifies` clause. module Trafo { resource struct R { x: u64 } public fun opaque_decr(addr: address) acquires R { let r = borrow_global_mut(addr); r.x = r.x - 1; } spec fun opaque_decr { pragma opaque; modifies global(addr); aborts_if !exists(addr); aborts_if global(addr).x == 0; ensures exists(addr); ensures global(addr).x == old(global(addr).x) - 1; } public fun opaque_caller(addr: address) acquires R { opaque_decr(addr); opaque_decr(addr); } spec fun opaque_caller { modifies global(addr); aborts_if !exists(addr); aborts_if global(addr).x < 2; ensures global(addr).x == old(global(addr).x) - 2; } } }