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] Test that non-Boolean literals are actually integers

Browse Source
This commit is contained in:
Leonardo Alt 2019-06-04 14:29:35 +02:00
parent d99c37e1ee
commit f281c94b42
2 changed files with 16 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolidity/formal/CVC4Interface.cpp
View File

@ -132,8 +132,14 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
else if (n == "false")
return m_context.mkConst(false);
else
// We assume it is an integer...
return m_context.mkConst(CVC4::Rational(n));
try
{
return m_context.mkConst(CVC4::Rational(n));
}
catch (...)
{
solAssert(false, "");
}
}
solAssert(_expr.hasCorrectArity(), "");

10
libsolidity/formal/Z3Interface.cpp
View File

@ -131,8 +131,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "false")
return m_context.bool_val(false);
else
// We assume it is an integer...
return m_context.int_val(n.c_str());
try
{
return m_context.int_val(n.c_str());
}
catch (...)
{
solAssert(false, "");
}
}
solAssert(_expr.hasCorrectArity(), "");