cerc-io/solidity
15
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] refactoring of resetting storage variables

Browse Source
This commit is contained in:
Martin Blicha 2021-02-03 11:42:20 +01:00
parent f1013427a7
commit d99256aae7
3 changed files with 2 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/BMC.cpp
View File

@ -561,8 +561,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
else else
{ {
m_externalFunctionCallHappened = true; m_externalFunctionCallHappened = true;
resetStateVariables(); resetStorageVariables();
resetStorageReferences();
} }
} }
@ -624,11 +623,6 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
return values; return values;
} }
void BMC::resetStorageReferences()
{
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
}
void BMC::reset() void BMC::reset()
{ {
m_externalFunctionCallHappened = false; m_externalFunctionCallHappened = false;

1
libsolidity/formal/BMC.h
View File

@ -123,7 +123,6 @@ private:
Expression const& _expression Expression const& _expression
) override; ) override;
void resetStorageReferences();
void reset(); void reset();
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions(); std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions();

3
libsolidity/formal/CHC.cpp
View File

@ -880,8 +880,7 @@ void CHC::resetContractAnalysis()
void CHC::eraseKnowledge() void CHC::eraseKnowledge()
{ {
resetStateVariables(); resetStorageVariables();
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
} }
void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)