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 bound function calls

Browse Source
This commit is contained in:
Leonardo Alt
2018-11-19 15:29:00 +01:00
parent 5be45e736d
commit 06c3f0953a
6 changed files with 91 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTChecker.cpp
+12
View File
@@ -457,6 +457,14 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
else if (_funDef && _funDef->isImplemented())
{
vector<smt::Expression> funArgs;
auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
solAssert(funType, "");
if (funType->bound())
{
auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
solAssert(boundFunction, "");
funArgs.push_back(expr(boundFunction->expression()));
}
for (auto arg: _funCall.arguments())
funArgs.push_back(expr(*arg));
initializeFunctionCallParameters(*_funDef, funArgs);
@@ -548,6 +556,10 @@ void SMTChecker::endVisit(Return const& _return)
bool SMTChecker::visit(MemberAccess const& _memberAccess)
{
auto const& accessType = _memberAccess.annotation().type;
if (accessType->category() == Type::Category::Function)
return true;
auto const& exprType = _memberAccess.expression().annotation().type;
solAssert(exprType, "");
if (exprType->category() == Type::Category::Magic)