[More Detail] [Collapse All]
Feature: Message call to unknown recipient


Ethereum yellow paper (Homestead revision) definitions 101-104
specify that if recipient account is originally undefined, it will
be created with no code or state and zero balance. Defitinitions
100 and 104 specify that value is transferred to the newly created
account
features/100-constructors/500-msg-call-to-unknown-recipient.feature
- Background: Create configuration with two source files
link
features/100-constructors/500-msg-call-to-unknown-recipient.feature:10
Given I create initial sbuilder context with:
Directory
solidity demo1
setup setup1
And a file named "solidity/demo1.sol" with:
pragma solidity >0.4.4;

contract Demo1 {

    uint storedData1;
    address owner1;

    function set(uint x) {
        storedData1 = x;
    }

    function get() constant returns (uint retVal) {
        return storedData1;
    }
}
- Scenario: Message call to non-existing contract account creates empty account
link
features/100-constructors/500-msg-call-to-unknown-recipient.feature:35
#
#  This scenario creates account 1, and mines 5 units ether.
#  In step 3, call Demo1(set) for non exisisting account,
#  results to creation of new account, with no code ('codeHash |->Nil),
#  and value of the call being transferred to the account ( balance |->3)
#
#
And a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 2

     - domain: eth_value
       range:  [0,5]

 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          input:
              value: 5
        - interface: Demo1(set)
          input:
                recipient: 2
                value: 3
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
1 step p_personal_newAccount__
2 step p_geth_mine__
3 eth_accounts balance 5
3 step p_Demo1_set_
3 eth_accounts address d_eth_address_1
3 eth_accounts address d_eth_address_2
3 eth_accounts d_eth_address_1 balance 2
3 eth_accounts d_eth_address_2 balance 3
3 eth_accounts d_eth_address_2 codeHash Nil