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] Avoid implicit conversion

Browse Source
This commit is contained in:
Alex Beregszaszi 2020-07-13 21:40:33 +01:00
parent 0f6d3bc4ed
commit 2f899bbffa
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::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override; std::vector<std::string> unhandledQueries() override;
unsigned solvers() override { return m_solvers.size(); } size_t solvers() override { return m_solvers.size(); }
private: private:
static bool solverAnswered(CheckResult result); static bool solverAnswered(CheckResult result);

2
libsmtutil/SolverInterface.h
View File

@ -402,7 +402,7 @@ public:
virtual std::vector<std::string> unhandledQueries() { return {}; } virtual std::vector<std::string> unhandledQueries() { return {}; }
/// @returns how many SMT solvers this interface has. /// @returns how many SMT solvers this interface has.
virtual unsigned solvers() { return 1; } virtual size_t solvers() { return 1; }
protected: protected:
std::optional<unsigned> m_queryTimeout; 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") else if (n == "int2bv")
{ {
size_t size = std::stoul(_expr.arguments[1].name); 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") else if (n == "bv2int")
{ {
@ -240,7 +240,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "tuple_get") else if (n == "tuple_get")
{ {
size_t index = stoul(_expr.arguments[1].name); 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") 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_vector projs(m_context);
z3::func_decl tupleConstructor = m_context.tuple_sort( z3::func_decl tupleConstructor = m_context.tuple_sort(
tupleSort.name.c_str(), tupleSort.name.c_str(),
tupleSort.members.size(), static_cast<unsigned>(tupleSort.members.size()),
cMembers.data(), cMembers.data(),
sorts.data(), sorts.data(),
projs projs

2
libsolidity/formal/EncodingContext.h
View File

@ -142,7 +142,7 @@ public:
void pushSolver(); void pushSolver();
void popSolver(); void popSolver();
void addAssertion(smtutil::Expression const& _e); void addAssertion(smtutil::Expression const& _e);
unsigned solverStackHeigh() { return m_assertions.size(); } const size_t solverStackHeigh() { return m_assertions.size(); } const
smtutil::SolverInterface* solver() smtutil::SolverInterface* solver()
{ {
solAssert(m_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; return false;
// Sometimes the solver assigns huge lengths that are not related, // Sometimes the solver assigns huge lengths that are not related,
// we should catch and ignore those. // we should catch and ignore those.
unsigned index; unsigned long index;
try try
{ {
index = stoul(*indexStr); index = stoul(*indexStr);

2
libsolidity/formal/SymbolicState.cpp
View File

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