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

Change CHC to avoid sign mismatch

Browse Source
This commit is contained in:
Alex Beregszaszi 2020-07-08 10:47:03 +01:00 committed by Djordje Mijovic
parent 547590b972
commit a0300835eb
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/CHC.cpp
View File

@ -990,13 +990,13 @@ vector<smtutil::Expression> CHC::initialStateVariables(ContractDefinition const&
return stateVariablesAtIndex(0, _contract); return stateVariablesAtIndex(0, _contract);
} }
vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index) vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
{ {
solAssert(m_currentContract, ""); solAssert(m_currentContract, "");
return stateVariablesAtIndex(_index, *m_currentContract); return stateVariablesAtIndex(_index, *m_currentContract);
} }
vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract) vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
{ {
return applyMap( return applyMap(
stateVariablesIncludingInheritedAndPrivate(_contract), stateVariablesIncludingInheritedAndPrivate(_contract),

4
libsolidity/formal/CHC.h
View File

@ -152,8 +152,8 @@ private:
/// of the current transaction. /// of the current transaction.
std::vector<smtutil::Expression> initialStateVariables(); std::vector<smtutil::Expression> initialStateVariables();
std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract); std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract);
std::vector<smtutil::Expression> stateVariablesAtIndex(int _index); std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index);
std::vector<smtutil::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract); std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract);
/// @returns the current symbolic values of the current state variables. /// @returns the current symbolic values of the current state variables.
std::vector<smtutil::Expression> currentStateVariables(); std::vector<smtutil::Expression> currentStateVariables();
std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract); std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);