a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
802 stars 65 forks source link

fix: manually solve dynamic array overflow conditions #366

Closed daejunpark closed 1 week ago

daejunpark commented 1 week ago

this pr fixes the false positive warnings of loop unrolling bounds, which were generated during the creation of storage arrays:

contract ATest {
    uint[] numbers;

    function setUp() {
        numbers = new uint[](5);
        ...
    }
}