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

Event tracking doesn't handle references #148

Open dddejan opened 4 years ago

dddejan commented 4 years ago
pragma solidity >=0.5.0;

contract EventTrackingStorageRef {

  mapping(address=>bool) data;

  /// @notice tracks-changes-in data
  event e(address a);

  /// @notice emits e
  function f(address a) public {
    mapping(address=>bool) storage ref = data;
    ref[a] = true;
  }
}

In the contract above, function f should emit the event but it doesn't, this should be reported as error. Current version says

$ ./solc-verify.py issue.sol --output .
EventTrackingStorageRef::f: OK
EventTrackingStorageRef::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
No errors found.

We need to check if the reference potentially updates the tracked data which is currently not done.