SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

Postcondition of function with function call not verifiable #165

Closed zhao-nan closed 4 years ago

zhao-nan commented 4 years ago

Description

pragma solidity >=0.5.0 <0.6.0;
contract Test {
  int res;

  /// @notice postcondition res == x + 1
  function callInc(int x) public returns (int) {
      res = inc(x);
  }

  /// @notice postcondition res == x + 1
  function inc(int x) public returns (int) {
      res = x+1;
  }
}

In the above contract, both function contracts should be verifiable. However, solc-verify reports that the first postcondition might not hold.

Test::callInc: ERROR
 - Test.sol:6:5: Postcondition 'res == x + 1' might not hold at end of function.

Environment

Semi-Related question

is it possible to refer to a function's return value? If so, how? In the above, I actually do not want a global res variable, but I could not find another way to express this.

dddejan commented 4 years ago

Function inc doesn't return anything, the way you wrote the contract both functions write into a state variable but always return zero.

dddejan commented 4 years ago

To refer to the return value you need to name the return value 'returns (int res)'.

dddejan commented 4 years ago

The following contract verifies fine

contract Test {
  /// @notice postcondition res == x + 1
  function callInc(int x) public returns (int res) {
      res = inc(x);
  }

  /// @notice postcondition res == x + 1
  function inc(int x) public returns (int res) {
      res = x+1;
  }
}