diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-10-25 23:50:31 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-11-19 22:29:00 +0800 |
| commit | 06c3f0953ae9f9921683f80349c7b1bbddcb3a9f (patch) | |
| tree | b671dcda3fca233f9213da5a217c83c6ddcf534e /libsolidity/formal | |
| parent | 5be45e736d2b111c9352ca2990a1c7a653c60c55 (diff) | |
| download | dexon-solidity-06c3f0953ae9f9921683f80349c7b1bbddcb3a9f.tar.gz dexon-solidity-06c3f0953ae9f9921683f80349c7b1bbddcb3a9f.tar.zst dexon-solidity-06c3f0953ae9f9921683f80349c7b1bbddcb3a9f.zip | |
[SMTChecker] Support bound function calls
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 9a2b9bbf..bbc78c0c 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -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) |