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 #10262 from ethereum/smt-conversion

Browse Source 
[SMTChecker] Avoid implicit conversion
This commit is contained in:
Alex Beregszaszi 2020-11-11 17:03:49 +00:00 committed by GitHub
commit 826ed58b2f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/SMTPortfolio.h
View File

@ -58,7 +58,7 @@ public:
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override;
unsigned solvers() override { return m_solvers.size(); }
size_t solvers() override { return m_solvers.size(); }
private:
static bool solverAnswered(CheckResult result);

2
libsmtutil/SolverInterface.h
View File

@ -402,7 +402,7 @@ public:
virtual std::vector<std::string> unhandledQueries() { return {}; }
/// @returns how many SMT solvers this interface has.
virtual unsigned solvers() { return 1; }
virtual size_t solvers() { return 1; }
protected:
std::optional<unsigned> m_queryTimeout;

6
libsmtutil/Z3Interface.cpp
View File

@ -217,7 +217,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "int2bv")
{
size_t size = std::stoul(_expr.arguments[1].name);
return z3::int2bv(size, arguments[0]);
return z3::int2bv(static_cast<unsigned>(size), arguments[0]);
}
else if (n == "bv2int")
{
@ -240,7 +240,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "tuple_get")
{
size_t index = stoul(_expr.arguments[1].name);
return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]);
return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), static_cast<unsigned>(index)))(arguments[0]);
}
else if (n == "tuple_constructor")
{
@ -367,7 +367,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
z3::func_decl_vector projs(m_context);
z3::func_decl tupleConstructor = m_context.tuple_sort(
tupleSort.name.c_str(),
tupleSort.members.size(),
static_cast<unsigned>(tupleSort.members.size()),
cMembers.data(),
sorts.data(),
projs

2
libsolidity/formal/EncodingContext.h
View File

@ -142,7 +142,7 @@ public:
void pushSolver();
void popSolver();
void addAssertion(smtutil::Expression const& _e);
unsigned solverStackHeigh() { return m_assertions.size(); } const
size_t solverStackHeigh() { return m_assertions.size(); } const
smtutil::SolverInterface* solver()
{
solAssert(m_solver, "");

2
libsolidity/formal/Predicate.cpp
View File

@ -349,7 +349,7 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
return false;
// Sometimes the solver assigns huge lengths that are not related,
// we should catch and ignore those.
unsigned index;
unsigned long index;
try
{
index = stoul(*indexStr);

2
libsolidity/formal/SymbolicState.cpp
View File

@ -41,7 +41,7 @@ BlockchainVariable::BlockchainVariable(
{
members.emplace_back(component);
sorts.emplace_back(sort);
m_componentIndices[component] = members.size() - 1;
m_componentIndices[component] = static_cast<unsigned>(members.size() - 1);
}
m_tuple = make_unique<SymbolicTupleVariable>(
make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),