False positives for actions on a reverting branch

[ritzdorf]

Consider the following example:

contract Wallet {

  uint balance;
  function send(){
    if (balance > 0){
      msg.sender.call.value(balance)();
      balance = 0;
    }
    revert();
  }
}

Securify reports violations for multiple patterns even though they cannot take place. In my intuition, the patterns (probably most securify patterns) are lacking something saying that this action, e.g. the storage write in case of the DAO pattern, may be followed by a STOP or RETURN.

[ptsankov]

Correct, all patterns assume that all instructions are reachable.

[ritzdorf]

@ptsankov thanks for the clarification. Which priority would you give this issue, given that most instructions will have some path to a non-reverting end of execution?

[ptsankov]

Close to zero, the assumption is reasonable, flagging dead code is fine, and to fix this precision issue we will need to integrate with the symbolic system which is pretty major.

[hiqua]

For this kind of dead code (variable is read-only so the branching can solved statically, at compilation time), the improvement arguably belongs more to the compiler (optimizer) rather than Securify itself, so it could make more sense to solve it there directly.