diff --git a/test/transactions/tokens/SomeTokenModified/RandomTransfer.ref b/test/transactions/tokens/SomeTokenModified/RandomTransfer.ref new file mode 100644 index 0000000..33d0f6e --- /dev/null +++ b/test/transactions/tokens/SomeTokenModified/RandomTransfer.ref @@ -0,0 +1,637 @@ + + + .K + + + false + + + + SomeTokenTest + + + .IfaceCellMap + + + + + SomeToken + + + UINT256_MAX |-> uint256 + _allowances |-> mapping ( address account => mapping ( address spender => uint256 ) ) + _balances |-> mapping ( address account => uint256 ) + _name |-> string + _symbol |-> string + _totalSupply |-> uint256 + + + ListItem ( UINT256_MAX = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff ; ) + + + + + _approve + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + ListItem ( bool ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + ListItem ( emitEvent ) + + + .List + + + .List + + + false + + + require ( owner != address ( 0 , .TypedVals ) , "SomeToken: invalid approver" , .TypedVals ) ; require ( spender != address ( 0 , .TypedVals ) , "SomeToken: invalid spender" , .TypedVals ) ; _allowances [ owner ] [ spender ] = value ; if ( emitEvent ) { emit Approval ( owner , spender , value , .TypedVals ) ; .Statements } .Statements + + + + _burn + + + private + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( account ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( account != address ( 0 , .TypedVals ) , "SomeToken: invalid sender" , .TypedVals ) ; _update ( account , address ( 0 , .TypedVals ) , value , .TypedVals ) ; .Statements + + + + _mint + + + private + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( account ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( account != address ( 0 , .TypedVals ) , "SomeToken: invalid receiver" , .TypedVals ) ; _update ( address ( 0 , .TypedVals ) , account , value , .TypedVals ) ; .Statements + + + + _spendAllowance + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + .List + + + .List + + + false + + + uint256 currentAllowance = allowance ( owner , spender , .TypedVals ) ; if ( currentAllowance != UINT256_MAX ) { require ( currentAllowance >= value , "SomeToken: insufficient allowance" , .TypedVals ) ; _approve ( owner , spender , currentAllowance - value , false , .TypedVals ) ; .Statements } .Statements + + + + _transfer + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + require ( from != address ( 0 , .TypedVals ) , "SomeToken: invalid sender" , .TypedVals ) ; require ( to != address ( 0 , .TypedVals ) , "SomeToken: invalid receiver" , .TypedVals ) ; _update ( from , to , value , .TypedVals ) ; .Statements + + + + _update + + + private + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + .List + + + .List + + + false + + + if ( from == address ( 0 , .TypedVals ) ) { _totalSupply = _totalSupply + value ; .Statements } else { uint256 fromBalance = _balances [ from ] ; require ( fromBalance >= value , "SomeToken: insufficient balance" , .TypedVals ) ; _balances [ from ] = fromBalance - value ; .Statements } if ( to == address ( 0 , .TypedVals ) ) { _totalSupply = _totalSupply - value ; .Statements } else { _balances [ to ] = _balances [ to ] + value ; .Statements } emit Transfer ( from , to , value , .TypedVals ) ; .Statements + + + + allowance + + + public + + + ListItem ( address ) + ListItem ( address ) + + + ListItem ( owner ) + ListItem ( spender ) + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return _allowances [ owner ] [ spender ] ; .Statements + + + + approve + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( spender ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address owner = msg . sender ; _approve ( owner , spender , value , true , .TypedVals ) ; return true ; .Statements + + + + balanceOf + + + public + + + ListItem ( address ) + + + ListItem ( account ) + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return _balances [ account ] ; .Statements + + + + constructor + + + public + + + ListItem ( uint256 ) + + + ListItem ( init_supply ) + + + .List + + + .List + + + false + + + _mint ( msg . sender , init_supply , .TypedVals ) ; .Statements + + + + decimals + + + public + + + .List + + + .List + + + ListItem ( uint8 ) + + + ListItem ( noId ) + + + false + + + return 18 ; .Statements + + + + name + + + public + + + .List + + + .List + + + ListItem ( string ) + + + ListItem ( noId ) + + + false + + + return _name ; .Statements + + + + symbol + + + public + + + .List + + + .List + + + ListItem ( string ) + + + ListItem ( noId ) + + + false + + + return _symbol ; .Statements + + + + totalSupply + + + public + + + .List + + + .List + + + ListItem ( uint256 ) + + + ListItem ( noId ) + + + false + + + return _totalSupply ; .Statements + + + + transfer + + + public + + + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address owner = msg . sender ; _transfer ( owner , to , value , .TypedVals ) ; return true ; .Statements + + + + transferFrom + + + public + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + ListItem ( bool ) + + + ListItem ( noId ) + + + false + + + address spender = msg . sender ; _spendAllowance ( from , spender , value , .TypedVals ) ; _transfer ( from , to , value , .TypedVals ) ; return true ; .Statements + + + + + + + Approval + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( owner ) + ListItem ( spender ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + Transfer + + + ListItem ( address ) + ListItem ( address ) + ListItem ( uint256 ) + + + ListItem ( from ) + ListItem ( to ) + ListItem ( value ) + + + SetItem ( 0 ) + SetItem ( 1 ) + + + + + + SomeTokenTest + + + _someToken |-> SomeToken + + + .List + + + + + _someToken + + + public + + + .List + + + .List + + + ListItem ( SomeToken ) + + + ListItem ( noId ) + + + false + + + return _someToken ; .Statements + + + + testERC20Transfer + + + public + + + .List + + + .List + + + .List + + + .List + + + false + + + uint256 _init_supply = 1e18 ; _someToken = new SomeToken ( _init_supply , .TypedVals ) ; uint256 _value = 100 ; _someToken . transfer ( address ( 0xdead , .TypedVals ) , _value , .TypedVals ) ; .Statements + + + + + .ContractEventCellMap + + + + + + + 1p160 + + + 0p256 + + + 1p160 + + + 1724300000p256 + + + 2p160 + + + SomeTokenTest + + + _init_supply |-> var ( 0 , uint256 ) + _value |-> var ( 1 , uint256 ) + + + ListItem ( 1000000000000000000p256 ) + ListItem ( 100p256 ) + + + testERC20Transfer + + + .List + + + + + 2p160 + + + SomeTokenTest + + + _someToken |-> 3p160 + + + + 3p160 + + + SomeToken + + + UINT256_MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256 + _balances |-> ( 2p160 |-> 999999999999999900p256 + 57005p160 |-> 100p256 ) + _totalSupply |-> 1000000000000000000p256 + + + + + 4p160 + + + diff --git a/test/transactions/tokens/SomeTokenModified/RandomTransfer.smr b/test/transactions/tokens/SomeTokenModified/RandomTransfer.smr new file mode 100644 index 0000000..c508d53 --- /dev/null +++ b/test/transactions/tokens/SomeTokenModified/RandomTransfer.smr @@ -0,0 +1 @@ +false