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

Merge pull request #10139 from ethereum/smt_fix_inherited_vars

Browse Source 
[SMTChecker] Fix inherited state vars for BMC
This commit is contained in:
Leonardo 2020-11-02 12:33:27 +00:00 committed by GitHub
commit b2f0c329e8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 19 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -12,6 +12,7 @@ Bugfixes:
* SMTChecker: Fix internal error when assigning state variable via contract's name.
* SMTChecker: Fix incorrect counterexamples reported by the CHC engine.
* SMTChecker: Fix false negative in modifier applied multiple times.
* SMTChecker: Fix internal error in the BMC engine when inherited contract from a different source unit has private state variables.
* Code generator: Fix missing creation dependency tracking for abstract contracts.

10
libsolidity/ast/AST.cpp
View File

@ -84,16 +84,6 @@ TypePointer ImportDirective::type() const
return TypeProvider::module(*annotation().sourceUnit);
}
vector<VariableDeclaration const*> ContractDefinition::stateVariablesIncludingInherited() const
{
vector<VariableDeclaration const*> stateVars;
for (auto const& contract: annotation().linearizedBaseContracts)
for (auto var: contract->stateVariables())
if (*contract == *this || var->isVisibleInDerivedContracts())
stateVars.push_back(var);
return stateVars;
}
bool ContractDefinition::derivesFrom(ContractDefinition const& _base) const
{
return util::contains(annotation().linearizedBaseContracts, &_base);

1
libsolidity/ast/AST.h
View File

@ -500,7 +500,6 @@ public:
std::vector<StructDefinition const*> definedStructs() const { return filteredNodes<StructDefinition>(m_subNodes); }
std::vector<EnumDefinition const*> definedEnums() const { return filteredNodes<EnumDefinition>(m_subNodes); }
std::vector<VariableDeclaration const*> stateVariables() const { return filteredNodes<VariableDeclaration>(m_subNodes); }
std::vector<VariableDeclaration const*> stateVariablesIncludingInherited() const;
std::vector<ModifierDefinition const*> functionModifiers() const { return filteredNodes<ModifierDefinition>(m_subNodes); }
std::vector<FunctionDefinition const*> definedFunctions() const { return filteredNodes<FunctionDefinition>(m_subNodes); }
std::vector<EventDefinition const*> events() const { return filteredNodes<EventDefinition>(m_subNodes); }

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -1973,7 +1973,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
{
for (auto var: _contract.stateVariablesIncludingInherited())
for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
createVariable(*var);
}
@ -2257,7 +2257,7 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
{
solAssert(_contract, "");
for (auto var: _contract->stateVariablesIncludingInherited())
for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
m_context.variable(*var)->resetIndex();
if (_function)
{

16
test/libsolidity/smtCheckerTests/imports/private_vars.sol Normal file
View File

@ -0,0 +1,16 @@
==== Source: ERC20.sol ====
pragma experimental SMTChecker;
contract ERC20 {
uint256 private a;
function f() internal virtual {
a = 2;
}
}
==== Source: Token.sol ====
pragma experimental SMTChecker;
import "ERC20.sol";
contract Token is ERC20 {
constructor() {
f();
}
}