cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

f

Browse Source
This commit is contained in:
Alex Beregszaszi 2020-09-23 23:29:27 +01:00
parent 726c5ff68c
commit 853175135e
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/SMTEncoder.cpp
View File

@ -664,6 +664,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
break;
case FunctionType::Kind::Send:
case FunctionType::Kind::Transfer:
case FunctionType::Kind::Selfdestruct:
{
auto const& memberAccess = dynamic_cast<MemberAccess const&>(_funCall.expression());
auto const& address = memberAccess.expression();
@ -674,6 +675,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
// Execution is stopped after selfdestruct.
if (funType.kind() == FunctionType::Kind::Selfdestruct)
addPathImplifiedExpression(smtutil::Expression(false));
break;
}
case FunctionType::Kind::ArrayPush: