test: multi test

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)
+   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

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;
+    }
 }
+