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 neither specified, nor emitted #141

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

This example passes, but should fail because f should emitchanged as it changes data.

contract C {
    mapping(int=>int) data;
    /// @notice tracks-changes-in data
    event changed();
    function f() public {
        data[0] = 1;
    }
}

Te problem is that we loop through all the declared emits for a function and add the event specs corresponding to those events. However, this way if the developer neither declares nor emits an event, the variable can still be changed. We should also loop through all the variables modified by the function and add the corresponding specs to detect such situations. If possible, it would be good to reuse AssignHelper for collecting variables because there are many tricky cases for assignments. (It's not enough to simply look for variables on LHS, e.g., x = y++).

dddejan commented 4 years ago

Should be fixed, close if it's OK.