In the function TranslateCallStatement (Sources/SolToBoogie/ProcedureTranslator.cs), the parameter outParams may be null. However, This code BoogieIdentifierExpr tmpVarExpr = outParams[0]; will call directly outParams[0] without judging whether the outParams is null.
Test Case( Test.sol ):
pragma solidity >=0.4.20;
contract Test {
function BugTest() public {
msg.sender.call.value(123)("");
}
}
ghost
commented
4 years ago
In the function TranslateCallStatement (Sources/SolToBoogie/ProcedureTranslator.cs), the parameter outParams may be null. However, This code BoogieIdentifierExpr tmpVarExpr = outParams[0]; will call directly outParams[0] without judging whether the outParams is null.
Test Case( Test.sol ):
pragma solidity >=0.4.20; contract Test { function BugTest() public { msg.sender.call.value(123)(""); } }