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

Merge pull request #6893 from ethereum/smt_int_lits

Browse Source 
[SMTChecker] Test that non-Boolean literals are actually integers
This commit is contained in:
Leonardo 2019-06-05 11:41:01 +02:00 committed by GitHub
commit d01c4195f8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 16 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/CVC4Interface.cpp
View File

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

8
libsolidity/formal/Z3Interface.cpp
View File

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