mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Style changes
This commit is contained in:
parent
89700dbcff
commit
8d65fd18fc
@ -688,7 +688,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
|
|||||||
{
|
{
|
||||||
auto const& memberAccess = dynamic_cast<MemberAccess const&>(_funCall.expression());
|
auto const& memberAccess = dynamic_cast<MemberAccess const&>(_funCall.expression());
|
||||||
auto const& address = memberAccess.expression();
|
auto const& address = memberAccess.expression();
|
||||||
auto const& value = args.at(0);
|
auto const& value = args.front();
|
||||||
solAssert(value, "");
|
solAssert(value, "");
|
||||||
|
|
||||||
smt::Expression thisBalance = m_context.balance();
|
smt::Expression thisBalance = m_context.balance();
|
||||||
@ -861,7 +861,7 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
|
|||||||
{
|
{
|
||||||
solAssert(_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
|
solAssert(_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
|
||||||
solAssert(_funCall.arguments().size() == 1, "");
|
solAssert(_funCall.arguments().size() == 1, "");
|
||||||
auto argument = _funCall.arguments().at(0);
|
auto argument = _funCall.arguments().front();
|
||||||
unsigned argSize = argument->annotation().type->storageBytes();
|
unsigned argSize = argument->annotation().type->storageBytes();
|
||||||
unsigned castSize = _funCall.annotation().type->storageBytes();
|
unsigned castSize = _funCall.annotation().type->storageBytes();
|
||||||
if (argSize == castSize)
|
if (argSize == castSize)
|
||||||
|
@ -134,8 +134,8 @@ vector<string> SMTPortfolio::unhandledQueries()
|
|||||||
// This code assumes that the constructor guarantees that
|
// This code assumes that the constructor guarantees that
|
||||||
// SmtLib2Interface is in position 0.
|
// SmtLib2Interface is in position 0.
|
||||||
solAssert(!m_solvers.empty(), "");
|
solAssert(!m_solvers.empty(), "");
|
||||||
solAssert(dynamic_cast<smt::SMTLib2Interface*>(m_solvers.at(0).get()), "");
|
solAssert(dynamic_cast<smt::SMTLib2Interface*>(m_solvers.front().get()), "");
|
||||||
return m_solvers.at(0)->unhandledQueries();
|
return m_solvers.front()->unhandledQueries();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool SMTPortfolio::solverAnswered(CheckResult result)
|
bool SMTPortfolio::solverAnswered(CheckResult result)
|
||||||
|
@ -47,7 +47,7 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
|
|||||||
// Abstract sort.
|
// Abstract sort.
|
||||||
returnSort = make_shared<smt::Sort>(smt::Kind::Int);
|
returnSort = make_shared<smt::Sort>(smt::Kind::Int);
|
||||||
else
|
else
|
||||||
returnSort = smtSort(*returnTypes.at(0));
|
returnSort = smtSort(*returnTypes.front());
|
||||||
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
|
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
|
||||||
}
|
}
|
||||||
case smt::Kind::Array:
|
case smt::Kind::Array:
|
||||||
|
Loading…
Reference in New Issue
Block a user