UnrestrictedWrite violation reported for unreachable code

[VeraBE]

I'm running Securify with Docker, I pulled the latest version, ran: sudo docker build . -t securify and then: sudo docker run -v $(pwd)/contracts:/project securify

The contracts folder only had this one:

pragma solidity ^0.4.24;

contract UnrestrictedWrite {
    bool public aVar;

    function aFunction(bool aParam) public {
        if (false) {
            aVar = aParam;
        }
    }
}

I get this in Securify's output:

Violation for UnrestrictedWrite in contract 'UnrestrictedWrite':
    |    function aFunction(bool aParam) public {
    |        if (false) {
  > |            aVar = aParam;
    |        }
    |    }
  at /project/UnrestrictedWrite_securify.sol(8)

[ptsankov]

Hi Vera, Securify doesn't perform symbolic analysis to identify that the assignment to aVar as unreachable. Hence it issues a false positive for your example.

[VeraBE]

Thanks for the quick reply!