tests: add tests from Act issue #184

tests/hevm/pass/cast-3/cast-3.act

@@ -0,0 +1,74 @@
+constructor of Token
+interface constructor(uint _supply)
+
+iff
+    CALLVALUE == 0
+
+creates
+    mapping(address => uint) balanceOf :=  [CALLER := _supply]
+
+behaviour balanceOf of Token
+interface balanceOf(address a)
+
+iff
+
+  CALLVALUE == 0
+
+returns pre(balanceOf[a])
+
+
+behaviour transfer of Token
+interface transfer(address to, uint256 value)
+
+iff
+
+  CALLVALUE == 0
+  CALLER =/= to => inRange(uint256, balanceOf[to] + value)
+  inRange(uint256,balanceOf[CALLER] - value)
+
+case CALLER =/= to:
+
+  storage
+
+    balanceOf[CALLER]  => balanceOf[CALLER] - value
+    balanceOf[to]    => balanceOf[to] + value
+
+  returns 1
+
+case CALLER == to:
+
+  returns 1
+
+
+constructor of TransferOneToken
+interface constructor(address _tokenAddress)
+
+iff
+
+    CALLVALUE == 0
+    _tokenAddress =/= 0
+
+creates
+
+    Token token := _tokenAddress as Token
+
+behaviour transfer of TransferOneToken
+interface transfer()
+
+iff
+    CALLVALUE == 0    
+    THIS =/= CALLER => inRange(uint256, token.balanceOf[CALLER] + 1)
+    inRange(uint256,token.balanceOf[THIS] - 1)
+
+case CALLER =/= THIS:
+
+storage
+
+    token.balanceOf[CALLER] => token.balanceOf[CALLER] + 1
+    token.balanceOf[THIS]  => token.balanceOf[THIS] - 1
+
+returns 1
+
+case CALLER == THIS:
+
+returns 1

tests/hevm/pass/cast-3/cast-3.sol

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract Token {
+    mapping (address => uint) public balanceOf;
+
+    constructor(uint _totalSupply) {
+        balanceOf[msg.sender] = _totalSupply;
+    }
+
+
+    function transfer(address to, uint256 value) public returns (uint) {
+	balanceOf[msg.sender] = balanceOf[msg.sender] - value;
+        balanceOf[to] = balanceOf[to] + value;
+        return 1;
+    }
+
+}
+
+
+
+contract TransferOneToken {
+    Token token;
+
+    constructor(address _tokenAddress) {
+        require(_tokenAddress != address(0), "Invalid token address");
+        token = Token(_tokenAddress);
+    }
+
+    function transfer() public returns (uint) {
+        // Transfer 1 token from the contract to the sender
+        uint256 transferAmt = 1;
+        token.transfer(msg.sender, transferAmt);
+	return 1;
+    }
+}