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

[SMTChecker] Add mod operator

Browse Source
This commit is contained in:
Leonardo Alt 2019-01-22 14:34:29 +01:00
parent 8992024302
commit 637546850f
3 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/CVC4Interface.cpp
View File

@ -163,6 +163,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
else if (n == "/")
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
else if (n == "mod")
return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
else if (n == "select")
return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
else if (n == "store")

5
libsolidity/formal/SolverInterface.h
View File

@ -141,6 +141,7 @@ public:
{"-", 2},
{"*", 2},
{"/", 2},
{"mod", 2},
{"select", 2},
{"store", 3}
};
@ -246,6 +247,10 @@ public:
{
return Expression("/", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator%(Expression _a, Expression _b)
{
return Expression("mod", std::move(_a), std::move(_b), Kind::Int);
}
Expression operator()(std::vector<Expression> _arguments) const
{
solAssert(

2
libsolidity/formal/Z3Interface.cpp
View File

@ -162,6 +162,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] * arguments[1];
else if (n == "/")
return arguments[0] / arguments[1];
else if (n == "mod")
return z3::mod(arguments[0], arguments[1]);
else if (n == "select")
return z3::select(arguments[0], arguments[1]);
else if (n == "store")