cerc-io/solidity
11
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 #9692 from ethereum/smt_fix_pop

Browse Source 
[SMTChecker] Fix soundness of array pop
This commit is contained in:
chriseth
2020-08-31 20:07:58 +02:00
committed by GitHub
parent b3b1df6556 8c05db88c0
commit 34543e5eab
11 changed files with 104 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+4 -4
View File
@@ -1111,11 +1111,11 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == oldElements);
auto newLength = smtutil::Expression::ite(
oldLength == 0,
smt::maxValue(*TypeProvider::uint256()),
oldLength - 1
oldLength > 0,
oldLength - 1,
0
);
m_context.addAssertion(symbArray->length() == oldLength - 1);
m_context.addAssertion(symbArray->length() == newLength);
arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
}