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 #11179 from ethereum/smt_fix_bfs_order

Browse Source 
[SMTChecker] Fix target warning order nondeterminism
This commit is contained in:
Leonardo 2021-03-26 14:00:47 +01:00 committed by GitHub
commit dcc0267cf4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
libsolidity/formal/CHC.cpp
View File

@ -920,10 +920,15 @@ void CHC::setCurrentBlock(Predicate const& _block)
set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
{
set<unsigned> verificationTargetsIds;
solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
verificationTargetsIds.insert(m_functionTargetIds[function].begin(), m_functionTargetIds[function].end());
for (auto const* called: m_callGraph[function])
_addChild(called);
struct ASTNodeCompare: EncodingContext::IdCompare
{
bool operator<(ASTNodeCompare _other) const { return operator()(node, _other.node); }
ASTNode const* node;
};
solidity::util::BreadthFirstSearch<ASTNodeCompare>{{{{}, _txRoot}}}.run([&](auto _node, auto&& _addChild) {
verificationTargetsIds.insert(m_functionTargetIds[_node.node].begin(), m_functionTargetIds[_node.node].end());
for (ASTNode const* called: m_callGraph[_node.node])
_addChild({{}, called});
});
return verificationTargetsIds;
}