I have a problem in understanding the code appeared in
the research paper: Cross-Contract Static Analysis for Detecting Practical Reentrancy Vulnerabilities in Smart Contracts at: https://yuleisui.github.io/publications/ase20.pdf
I think that condition on line#5 should be false in any case in order to accomplish the transfer in line#9. But the paper says that:
However, in practice, such path in CFG to exercise the chain can never be feasible. The
reason is that○5 →○7 requires reEntered = true while○? →○5→○7 requires reEntered = false. They are contradictory.
We have the following code shown in the attached image:
Somebody please guide me.