search

Certora / tutorials-code

Certora tutorials
MIT License
19 stars 24 forks source link

Missing Spec for BordaNewBug #11

Open D4r3-D3v1L opened 1 year ago

D4r3-D3v1L commented 1 year ago

Link to PR : https://github.com/Certora/tutorials-code/pull/9

A run of the new BordaMissingRule.spec on Borda.sol https://prover.certora.com/output/95406/ad390610904f490fb14c8a39d244a929?anonymousKey=8da1cada70decf9448a2a7fad759cf69e3fdb464

A run on the Borda.spec on BordaNewBug.sol https://prover.certora.com/output/95406/a94453aaf96f40cab8c20bb9ca1a208f?anonymousKey=55dfe859583816dabe226c6f105bcba758a2fd9c

A run on the BordaMissingRule.spec on BordaNewBug.sol https://prover.certora.com/output/95406/cf90c05695cd4c9a8f01da8ac2cb5e22?anonymousKey=9ffe665d58643a3ad573d1b73f3e7b118f82de13

nd-certora commented 1 year ago

This is not acknowledged as there is no effect on the winner from the point of view of the IBorda interface . If you could have:

    function points(address c) public view override returns (uint256) {
      if (c == winner)
           return pointsOfWinner;
        return _points[c];
    }

It would have been caught by the existing spec. you are welcome to try more if there are still no five acknowledged