diff --git a/contracts/IoTeXNetwork.sol b/contracts/IoTeXNetwork.sol index 1245707..c1c2723 100755 --- a/contracts/IoTeXNetwork.sol +++ b/contracts/IoTeXNetwork.sol @@ -24,28 +24,80 @@ contract IoTeXNetwork is StandardToken, Pausable { emit Transfer(address(0x0), msg.sender, tokenTotalAmount); } + /*@CTK CtkTransferNoEffect + @post (_to == address(0)) \/ (paused == true) -> __reverted == true + */ + /*@CTK CtkTransferEffect + @pre __reverted == false + @pre balances[msg.sender] >= _value + @pre paused == false + @pre __return == true + @pre msg.sender != _to + @post __post.balances[_to] == balances[_to] + _value + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function transfer(address _to, uint _value) whenNotPaused validDestination(_to) returns (bool) { return super.transfer(_to, _value); } + /*@CTK CtkTransferFromNoEffect + @post (_to == address(0)) \/ (paused == true) -> __reverted == true + */ + /*@CTK CtkTransferFromEffect + @tag assume_completion + @pre _from != _to + @post __post.balances[_to] == balances[_to] + _value + @post __post.balances[_from] == balances[_from] - _value + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function transferFrom(address _from, address _to, uint _value) whenNotPaused validDestination(_to) returns (bool) { return super.transferFrom(_from, _to, _value); } + /*@CTK CtkApproveNoEffect + @post (paused == true) -> __post == this + */ + /*@CTK CtkApprove + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == _value + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function approve(address _spender, uint256 _value) public whenNotPaused returns (bool) { return super.approve(_spender, _value); } + /*@CTK CtkIncreaseApprovalNoEffect + @post (paused == true) -> __reverted == true + */ + /*@CTK CtkIncreaseApprovalEffect + @pre paused == false + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] + _addedValue + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function increaseApproval(address _spender, uint _addedValue) public whenNotPaused returns (bool success) { return super.increaseApproval(_spender, _addedValue); } + /*@CTK CtkDecreaseApprovalNoEffect + @post (paused == true) -> __reverted == true + */ + /*@CTK CtkDecreaseApprovalEffect + @pre allowed[msg.sender][_spender] >= _subtractedValue + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] - _subtractedValue + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function decreaseApproval(address _spender, uint _subtractedValue) public whenNotPaused returns (bool success) { return super.decreaseApproval(_spender, _subtractedValue); diff --git a/contracts/Migrations.sol b/contracts/Migrations.sol index dd89466..a193ff8 100644 --- a/contracts/Migrations.sol +++ b/contracts/Migrations.sol @@ -8,10 +8,19 @@ contract Migrations { if (msg.sender == owner) _; } + /*@CTK init_migrations + @post __post.owner == msg.sender + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function Migrations() public { owner = msg.sender; } + /*@CTK set_complete + @pre msg.sender == owner + @post __post.last_completed_migration == completed + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function setCompleted(uint completed) public restricted { last_completed_migration = completed; } @@ -20,4 +29,4 @@ contract Migrations { Migrations upgraded = Migrations(new_address); upgraded.setCompleted(last_completed_migration); } -} \ No newline at end of file +} diff --git a/contracts/math/SafeMath.sol b/contracts/math/SafeMath.sol index c119270..dd6c12f 100755 --- a/contracts/math/SafeMath.sol +++ b/contracts/math/SafeMath.sol @@ -10,6 +10,15 @@ library SafeMath { /** * @dev Multiplies two numbers, throws on overflow. */ + + /*@CTK SafeMath_mul + @tag spec + @post __reverted == __has_assertion_failure + @post __has_assertion_failure == __has_overflow + @post __reverted == false -> c == a * b + @post msg == msg__post + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function mul(uint256 a, uint256 b) internal pure returns (uint256 c) { if (a == 0) { return 0; @@ -22,6 +31,15 @@ library SafeMath { /** * @dev Integer division of two numbers, truncating the quotient. */ + /*@CTK SafeMath_div + @tag spec + @pre b != 0 + @post __reverted == __has_assertion_failure + @post __has_overflow == true -> __has_assertion_failure == true + @post __reverted == false -> __return == a / b + @post msg == msg__post + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function div(uint256 a, uint256 b) internal pure returns (uint256) { // assert(b > 0); // Solidity automatically throws when dividing by 0 // uint256 c = a / b; @@ -32,6 +50,14 @@ library SafeMath { /** * @dev Subtracts two numbers, throws on overflow (i.e. if subtrahend is greater than minuend). */ + /*@CTK SafeMath_sub + @tag spec + @post __reverted == __has_assertion_failure + @post __has_overflow == true -> __has_assertion_failure == true + @post __reverted == false -> __return == a - b + @post msg == msg__post + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function sub(uint256 a, uint256 b) internal pure returns (uint256) { assert(b <= a); return a - b; @@ -40,9 +66,17 @@ library SafeMath { /** * @dev Adds two numbers, throws on overflow. */ + /*@CTK SafeMath_add + @tag spec + @post __reverted == __has_assertion_failure + @post __has_assertion_failure == __has_overflow + @post __reverted == false -> c == a + b + @post msg == msg__post + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function add(uint256 a, uint256 b) internal pure returns (uint256 c) { c = a + b; assert(c >= a); return c; } -} \ No newline at end of file +} diff --git a/contracts/ownership/Ownable.sol b/contracts/ownership/Ownable.sol index 7e73b78..56cbc55 100755 --- a/contracts/ownership/Ownable.sol +++ b/contracts/ownership/Ownable.sol @@ -17,6 +17,10 @@ contract Ownable { * @dev The Ownable constructor sets the original `owner` of the contract to the sender * account. */ + /*@CTK owner_set_on_success + @pre __reverted == false -> __post.owner == owner + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function Ownable() public { owner = msg.sender; } @@ -33,10 +37,16 @@ contract Ownable { * @dev Allows the current owner to transfer control of the contract to a newOwner. * @param newOwner The address to transfer ownership to. */ + /*@CTK transferOwnership + @post __reverted == false -> (msg.sender == owner -> __post.owner == newOwner) + @post (owner != msg.sender) -> (__reverted == true) + @post (newOwner == address(0)) -> (__reverted == true) + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function transferOwnership(address newOwner) public onlyOwner { require(newOwner != address(0)); emit OwnershipTransferred(owner, newOwner); owner = newOwner; } -} \ No newline at end of file +} diff --git a/contracts/token/BasicToken.sol b/contracts/token/BasicToken.sol index bb315f4..97b4755 100755 --- a/contracts/token/BasicToken.sol +++ b/contracts/token/BasicToken.sol @@ -28,6 +28,25 @@ contract BasicToken is ERC20Basic { * @param _to The address to transfer to. * @param _value The amount to be transferred. */ + /*@CTK transfer_success + @pre _to != address(0) + @pre balances[msg.sender] >= _value + @pre __reverted == false + @post __reverted == false + @post __return == true + */ + /*@CTK transfer_same_address + @tag no_overflow + @pre _to == msg.sender + @post this == __post + */ + /*@CTK transfer_conditions + @tag assume_completion + @pre _to != msg.sender + @post __post.balances[_to] == balances[_to] + _value + @post __post.balances[msg.sender] == balances[msg.sender] - _value + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function transfer(address _to, uint256 _value) public returns (bool) { require(_to != address(0)); require(_value <= balances[msg.sender]); @@ -43,8 +62,13 @@ contract BasicToken is ERC20Basic { * @param _owner The address to query the the balance of. * @return An uint256 representing the amount owned by the passed address. */ + /*@CTK balanceOf + @post __reverted == false + @post __return == balances[_owner] + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function balanceOf(address _owner) public view returns (uint256) { return balances[_owner]; } -} \ No newline at end of file +} diff --git a/contracts/token/StandardToken.sol b/contracts/token/StandardToken.sol index 724fcc8..c609453 100755 --- a/contracts/token/StandardToken.sol +++ b/contracts/token/StandardToken.sol @@ -22,6 +22,15 @@ contract StandardToken is ERC20, BasicToken { * @param _to address The address which you want to transfer to * @param _value uint256 the amount of tokens to be transferred */ + /*@CTK transferFrom + @tag assume_completion + @pre _from != _to + @post __return == true + @post __post.balances[_to] == balances[_to] + _value + @post __post.balances[_from] == balances[_from] - _value + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function transferFrom(address _from, address _to, uint256 _value) public returns (bool) { require(_to != address(0)); require(_value <= balances[_from]); @@ -44,6 +53,15 @@ contract StandardToken is ERC20, BasicToken { * @param _spender The address which will spend the funds. * @param _value The amount of tokens to be spent. */ + /*@CTK approve_success + @post _value == 0 -> __reverted == false + @post allowed[msg.sender][_spender] == 0 -> __reverted == false + */ + /*@CTK approve + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == _value + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function approve(address _spender, uint256 _value) public returns (bool) { allowed[msg.sender][_spender] = _value; emit Approval(msg.sender, _spender, _value); @@ -70,6 +88,12 @@ contract StandardToken is ERC20, BasicToken { * @param _spender The address which will spend the funds. * @param _addedValue The amount of tokens to increase the allowance by. */ + /*@CTK CtkIncreaseApprovalEffect + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] + _addedValue + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function increaseApproval(address _spender, uint _addedValue) public returns (bool) { allowed[msg.sender][_spender] = allowed[msg.sender][_spender].add(_addedValue); emit Approval(msg.sender, _spender, allowed[msg.sender][_spender]); @@ -86,6 +110,19 @@ contract StandardToken is ERC20, BasicToken { * @param _spender The address which will spend the funds. * @param _subtractedValue The amount of tokens to decrease the allowance by. */ + /*@CTK CtkDecreaseApprovalEffect_1 + @pre allowed[msg.sender][_spender] >= _subtractedValue + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] - _subtractedValue + @post __has_overflow == false + */ + /*@CTK CtkDecreaseApprovalEffect_2 + @pre allowed[msg.sender][_spender] < _subtractedValue + @tag assume_completion + @post __post.allowed[msg.sender][_spender] == 0 + @post __has_overflow == false + */ + /* CertiK Smart Labelling, for more details visit: https://certik.org */ function decreaseApproval(address _spender, uint _subtractedValue) public returns (bool) { uint oldValue = allowed[msg.sender][_spender]; if (_subtractedValue > oldValue) { @@ -97,4 +134,4 @@ contract StandardToken is ERC20, BasicToken { return true; } -} \ No newline at end of file +}