cerc-io/solidity
10
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

Use the nondeterministic interface also for BARECALL

Browse Source
This commit is contained in:
Leo Alt 2021-08-11 18:10:21 +02:00
parent 45a910c2ca
commit d89d63bf9c
2 changed files with 17 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
libsolidity/formal/CHC.cpp
View File

@ -529,11 +529,11 @@ void CHC::endVisit(FunctionCall const& _funCall)
break; break;
case FunctionType::Kind::External: case FunctionType::Kind::External:
case FunctionType::Kind::BareStaticCall: case FunctionType::Kind::BareStaticCall:
case FunctionType::Kind::BareCall:
externalFunctionCall(_funCall); externalFunctionCall(_funCall);
SMTEncoder::endVisit(_funCall); SMTEncoder::endVisit(_funCall);
break; break;
case FunctionType::Kind::DelegateCall: case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::Creation: case FunctionType::Kind::Creation:
@ -746,23 +746,29 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind(); auto kind = funType.kind();
solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); solAssert(
kind == FunctionType::Kind::External ||
kind == FunctionType::Kind::BareCall ||
kind == FunctionType::Kind::BareStaticCall,
""
);
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall;
solAssert(m_currentContract, ""); solAssert(m_currentContract, "");
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (!function) if (function)
return; {
usesStaticCall |= function->stateMutability() == StateMutability::Pure ||
for (auto var: function->returnParameters()) function->stateMutability() == StateMutability::View;
m_context.variable(*var)->increaseIndex(); for (auto var: function->returnParameters())
m_context.variable(*var)->increaseIndex();
}
if (!m_currentFunction || m_currentFunction->isConstructor()) if (!m_currentFunction || m_currentFunction->isConstructor())
return; return;
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(); auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
function->stateMutability() == StateMutability::Pure ||
function->stateMutability() == StateMutability::View;
if (!usesStaticCall) if (!usesStaticCall)
{ {

2
libsolidity/formal/SMTEncoder.cpp
View File

@ -611,6 +611,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
break; break;
case FunctionType::Kind::Internal: case FunctionType::Kind::Internal:
case FunctionType::Kind::BareStaticCall: case FunctionType::Kind::BareStaticCall:
case FunctionType::Kind::BareCall:
break; break;
case FunctionType::Kind::KECCAK256: case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover: case FunctionType::Kind::ECRecover:
@ -653,7 +654,6 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
visitObjectCreation(_funCall); visitObjectCreation(_funCall);
return; return;
case FunctionType::Kind::DelegateCall: case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::Creation: case FunctionType::Kind::Creation: