cerc-io/solidity
11
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

[SMTChecker] Support selfdestruct

Browse Source
This commit is contained in:
Leo Alt 2022-05-15 16:46:35 +02:00
parent 88573dbe03
commit fc957ee59b
3 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/formal/CHC.cpp
View File

@ -602,6 +602,7 @@ void CHC::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::MulMod:
case FunctionType::Kind::Unwrap:
case FunctionType::Kind::Wrap:
case FunctionType::Kind::Selfdestruct:
[[fallthrough]];
default:
SMTEncoder::endVisit(_funCall);

12
libsolidity/formal/SMTEncoder.cpp
View File

@ -714,6 +714,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
" with the CHC engine."
);
break;
case FunctionType::Kind::Selfdestruct:
visitSelfDestruct(_funCall);
break;
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall:
@ -917,6 +920,15 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
m_context.addAssertion(symbArray->elements() == zeroElements);
}
void SMTEncoder::visitSelfDestruct(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1);
solAssert(args.at(0));
state().transfer(state().thisAddress(), expr(*args.at(0)), state().balance(state().thisAddress()));
}
void SMTEncoder::endVisit(Identifier const& _identifier)
{
if (auto decl = identifierToVariable(_identifier))

1
libsolidity/formal/SMTEncoder.h
View File

@ -216,6 +216,7 @@ protected:
virtual void visitAddMulMod(FunctionCall const& _funCall);
void visitWrapUnwrap(FunctionCall const& _funCall);
void visitObjectCreation(FunctionCall const& _funCall);
void visitSelfDestruct(FunctionCall const& _funCall);
void visitTypeConversion(FunctionCall const& _funCall);
void visitStructConstructorCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);