diff --git a/tests/hevm/pass/multi3/multi3.act b/tests/hevm/pass/multi3/multi3.act index 8963253f..28b54f7c 100644 --- a/tests/hevm/pass/multi3/multi3.act +++ b/tests/hevm/pass/multi3/multi3.act @@ -20,6 +20,17 @@ iff returns pre(x) +behaviour add_x of A +interface add_x(uint y) + +iff + CALLVALUE == 0 + inRange(uint256, x + y) + +storage + + x => x + y + // contract B constructor of B @@ -30,6 +41,29 @@ iff creates uint z := i + 42 + A a := create A(i) + +behaviour incr_z of B +interface incr_z() + +iff + CALLVALUE == 0 + inRange(uint256, z + 1) + +storage + + z => z + 1 + +behaviour a_add_x of B +interface a_add_x(uint y) + +iff + CALLVALUE == 0 + inRange(uint256, a.x + y) + +storage + + a.x => a.x + y // contract C @@ -44,4 +78,20 @@ iff creates uint y := 0 A a := create A(u) - B b := create B(u) \ No newline at end of file + B b := create B(u) + + +behaviour remote of C +interface remote(uint z) + +iff + CALLVALUE == 0 + inRange(uint256, b.z + 1) + inRange(uint256, b.a.x + z) + +storage + + b.z => b.z + 1 + b.a.x => b.a.x + z + +returns z \ No newline at end of file diff --git a/tests/hevm/pass/multi3/multi3.sol b/tests/hevm/pass/multi3/multi3.sol index eebf41e9..4365d0d7 100644 --- a/tests/hevm/pass/multi3/multi3.sol +++ b/tests/hevm/pass/multi3/multi3.sol @@ -4,15 +4,28 @@ contract A { constructor (uint z) { x = z + 1; } + + function add_x(uint y) public { + x = x + y; + } } contract B { uint z; + A a; constructor (uint i) { z = i + 42; + a = new A(i); + } + + function incr_z() public { + z = z + 1; } + function a_add_x(uint y) public { + a.add_x(y); + } } contract C { @@ -26,4 +39,11 @@ contract C { a = new A(u); b = new B(u); } + + function remote(uint z) public returns (uint) { + b.incr_z(); + b.a_add_x(z); + return z; + } } +