aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <c@ethdev.com>2015-11-23 07:57:58 +0800
committerchriseth <c@ethdev.com>2015-11-23 07:58:17 +0800
commit806507d5c0a12c64771d2611487cb100f88fe4ff (patch)
tree228db1109dd299fef3203eaad018a707e59910bc /libsolidity
parent82a6ab486d6ee1fa565db1d0b02f2b34c855e796 (diff)
downloaddexon-solidity-806507d5c0a12c64771d2611487cb100f88fe4ff.tar.gz
dexon-solidity-806507d5c0a12c64771d2611487cb100f88fe4ff.tar.zst
dexon-solidity-806507d5c0a12c64771d2611487cb100f88fe4ff.zip
addmod and mulmod for why3.
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/Why3Translator.cpp53
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)