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

CHC clears indices so that initial is 0 and current is 1

Browse Source
This commit is contained in:
Leonardo Alt 2020-02-11 22:12:42 -03:00
parent 34d64761d9
commit d31a2a8d21
3 changed files with 19 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolidity/formal/CHC.cpp
View File

@ -505,6 +505,23 @@ void CHC::eraseKnowledge()
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
} }
void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
{
SMTEncoder::clearIndices(_contract, _function);
for (auto const* var: m_stateVariables)
/// SSA index 0 is reserved for state variables at the beginning
/// of the current transaction.
m_context.variable(*var)->increaseIndex();
if (_function)
{
for (auto const& var: _function->parameters() + _function->returnParameters())
m_context.variable(*var)->increaseIndex();
for (auto const& var: _function->localVariables())
m_context.variable(*var)->increaseIndex();
}
}
bool CHC::shouldVisit(ContractDefinition const& _contract) const bool CHC::shouldVisit(ContractDefinition const& _contract) const
{ {
if ( if (

1
libsolidity/formal/CHC.h
View File

@ -83,6 +83,7 @@ private:
//@{ //@{
void reset(); void reset();
void eraseKnowledge(); void eraseKnowledge();
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
bool shouldVisit(ContractDefinition const& _contract) const; bool shouldVisit(ContractDefinition const& _contract) const;
bool shouldVisit(FunctionDefinition const& _function) const; bool shouldVisit(FunctionDefinition const& _function) const;
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr); void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);

2
libsolidity/formal/SMTEncoder.h
View File

@ -217,7 +217,7 @@ protected:
/// Resets the variable indices. /// Resets the variable indices.
void resetVariableIndices(VariableIndices const& _indices); void resetVariableIndices(VariableIndices const& _indices);
/// Used when starting a new block. /// Used when starting a new block.
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr); virtual void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr);
/// @returns variables that are touched in _node's subtree. /// @returns variables that are touched in _node's subtree.