question: detection of reentrancy and unchecked send vulnerability

[yxliang01]

May I know whether it's possible to detect reentrancy and unchecked send vulnerability with this toolchain?

In the test cases, I can see DAO-buggy.sol has an assertion on the balance to avoid getting excessive amount of currency. However, such assertion is specifically for this instance of reentrancy and can't really be generalized.

[yxliang01]

Hi @shuvendu-lahiri , would you like to answer this question?

[shuvendu-lahiri]

There is no general support for reentrancy assertions in Verisol.

[yxliang01]

Thank you very much @shuvendu-lahiri for your reply. Would you also like to comment about the possibility of checking unchecked send vulnerabilities with this toolchain?