search

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

Wrong report with local pointer to multidimensional array #106

Closed dddejan closed 5 years ago

dddejan commented 5 years ago 
pragma solidity >=0.5.0;

contract Test {

    int[][] s;

    function test() public {
        require(s.length > 0 && s[0].length > 0);
        s[0][0] = 1;
        int[][] storage sl = s;
        assert(sl[0][0] == 1);
    }
}

Currently:

solc-verify.py Test.sol --output .
AssignArrayDynamicMultiL2L::test: ERROR
 - Test.sol:11:9: Assertion might not hold.
AssignArrayDynamicMultiL2L::[implicit_constructor]: OK
Errors were found by the verifier.
hajduakos commented 5 years ago

Fixed in 6f21e18bde597cab666db1f129b705c30b5f5b94