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

addmod and mulmod for why3.

Browse Source
This commit is contained in:
chriseth 2015-11-23 00:57:58 +01:00
parent 82a6ab486d
commit 806507d5c0
1 changed files with 38 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
libsolidity/formal/Why3Translator.cpp
View File

@ -465,11 +465,25 @@ 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;
case FunctionType::Location::AddMod:
case FunctionType::Location::MulMod:
{
//@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.");
@ -489,6 +503,11 @@ bool Why3Translator::visit(FunctionCall const& _node)
add(")");
return false;
}
default:
error(_node, "Only internal function calls supported.");
return true;
}
}
bool Why3Translator::visit(MemberAccess const& _node)
{