Conditional part of modifies should refer to old value

[hajduakos]

Currently, the if part of a modifies spec is directly translated into a postcondition, meaning that it will refer to the new values (unless manually adding old(...)). As discussed in #78, it should refer to the old values by default.

For example, this should not fail:

$ cat test.sol && solc-verify.py test.sol 
pragma solidity >=0.5.0;

contract Test {
    bool marked;

    /// @notice modifies marked if !marked
    function mark() public {
        require(!marked);
        marked = true;
    }
}
Test::mark: ERROR
 - test.sol:7:5: Function might modify 'marked' illegally
Test::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
Errors were found by the verifier.

[hajduakos]

Don't forget to update docs

[hajduakos]

Done in 82ded5d2043b594415abe8c188ed4bae8e5e86aa

@beillahi @michael-emmi this is some slight change to the annotation language. If you have modifies VAR if COND, then variables in COND will refer to the old values.

[michael-emmi]

Does that mean that there’s no way to say that something changed depending on the return value?

That situation actually something common to many APIs like collections. For instance, the Boolean return value of a Set.add operation would reflect whether the set changed. It might be nice to say that nothing was modified unless the return value is true. The condition would be more difficult to capture using only pre-state predicates.

[hajduakos]

Return value is a good point. But for the rest of the variables, preconditions make more sense to me. What about introducing two kind of conditions:

• modifies VAR if pre COND
• modifies VAR if post COND

This would also allow mixed pre/postconditions by using post in combination with old(...).

@dddejan ?

[dddejan]

Would it be ok to have the if condition over

• old values of state variables, and
• return value.

I feel that talking about modification where condition is using new values is somehow confusingly self-referential.

[michael-emmi]

That sounds reasonable to me.