[More Detail] [Collapse All]
Feature: Local variable
features/010-solidity/020-local-variable.feature
- Background: Define contract with functions
link
features/010-solidity/020-local-variable.feature:3
Given I create initial sbuilder context with:
Directory
solidity Demo1
setup setup1
And a file named "solidity/Demo1.sol" with:
pragma solidity >0.4.0;

contract Demo1 {

    uint public mostSent;

    function Demo1()  {
        uint amnt = msg.value;
        mostSent = amnt;
    }

}
- Scenario: Create a contract with mapping variable
link

This scenario calls 'Demo1' constructor with
msg.value=3. Constructor first assigns msg.value local variable
'amnt', next assigns it to contract variable 'mostSent'

State space extract:

eth_storageRoot@3={ [address |-> "d_eth_address_1"],
                    [address |-> "d_eth_address_2", mostSent |-> 3] }
features/010-solidity/020-local-variable.feature:27
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 3

       # Ether value range - later used non-deterministic choice
     - domain: eth_value
       range: [0,3]

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:
  
        - interface: personal_newAccount()
        - interface: geth_mine()
         
        # create contract 'Demo1' and use msg.value=3

        - interface: Demo1()
          input: 
              sender: 1
              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
3 eth_storageRoot d_eth_address_2 mostSent 3