An incorrect warning result

[sarser2048]

Description

I used Mythril to detect bugs in a smart contract, but received an incorrect analysis result. This detection module is based on the taint analysis.

Input File

Filename: EnvCase.sol

pragma solidity ^0.8.21;
contract EnvCase {
    uint public pastBlockTime;
    constructor() {}
    receive() external payable {}
    fallback() external payable {
        require(msg.value == 1 ether);
        pastBlockTime = block.timestamp + 5;
        if(pastBlockTime % 15 == 0) { // winner
            payable(msg.sender).transfer(address(this).balance);
        }
    }
}

How to Reproduce

Directly use the command myth analyze EnvCase.sol and you will get the analysis report.

$ myth analyze EnvCase.sol
==== Dependence on predictable environment variable ====
SWC ID: 116
Severity: Low
Contract: EnvCase
Function name: fallback
Estimated Gas Usage: 235 - 330
A control flow decision is made based on The block.timestamp environment variable......
--------------------
In file: #utility.yul:9

if gt(x, sum) { panic_error_0x11() }

--------------------
Initial State:

Account: [CREATOR], balance: 0x0, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}

Transaction Sequence:

Caller: [CREATOR], calldata: , decoded_data: , value: 0x0
Caller: [SOMEGUY], function: unknown, txdata: 0x00, decoded_data: , value: 0xde0b6b3a7640000

Expected behavior

Mythril should provide the correct file and location information of the detected bug, like:

In file: EnvCase.sol:9
    if(pastBlockTime % 15 == 0) { // winner

Environment

• Mythril version: 0.24.0
• Solidity compiler and version: 0.8.21
• Python version: 3.9.13
• OS and Version: MacOS