diff options
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 53 |
1 files changed, 36 insertions, 17 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 8a3b767b..cd036662 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -465,29 +465,48 @@ bool Why3Translator::visit(FunctionCall const& _node) return true; } FunctionType const& function = dynamic_cast<FunctionType const&>(*_node.expression().annotation().type); - if (function.location() != FunctionType::Location::Internal) + switch (function.location()) { - error(_node, "Only internal function calls supported."); - return true; - } - if (!_node.names().empty()) + case FunctionType::Location::AddMod: + case FunctionType::Location::MulMod: { - error(_node, "Function calls with named arguments not supported."); - return true; + //@todo require that third parameter is not zero + add("(of_int (mod (Int.("); + add(function.location() == FunctionType::Location::AddMod ? "+" : "*"); + add(") (to_int "); + _node.arguments().at(0)->accept(*this); + add(") (to_int "); + _node.arguments().at(1)->accept(*this); + add(")) (to_int "); + _node.arguments().at(2)->accept(*this); + add(")))"); + return false; } + case FunctionType::Location::Internal: + { + if (!_node.names().empty()) + { + error(_node, "Function calls with named arguments not supported."); + return true; + } - //@TODO check type conversions + //@TODO check type conversions - add("("); - _node.expression().accept(*this); - add(" state"); - for (auto const& arg: _node.arguments()) - { - add(" "); - arg->accept(*this); + add("("); + _node.expression().accept(*this); + add(" state"); + for (auto const& arg: _node.arguments()) + { + add(" "); + arg->accept(*this); + } + add(")"); + return false; + } + default: + error(_node, "Only internal function calls supported."); + return true; } - add(")"); - return false; } bool Why3Translator::visit(MemberAccess const& _node) |