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 #10750 from blishko/issue-10657

Browse Source 
[SMTChecker] Fixed pushing string literal to bytes array
This commit is contained in:
Leonardo 2021-01-13 17:28:42 +01:00 committed by GitHub
commit 501461147e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 23 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -18,6 +18,7 @@ Bugfixes:
* SMTChecker: Fix false negatives when analyzing external function calls.
* SMTChecker: Fix missing type constraints for block variables.
* SMTChecker: Fix internal error on ``block.chainid``.
* SMTChecker: Fix internal error on pushing string literal to ``bytes`` array.
* Type Checker: Fix internal error caused by constant structs containing mappings.
* Type System: Disallow implicit conversion from ``uintN`` to ``intM`` when ``M > N``, and by extension, explicit conversion between the same types is also disallowed.

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -1547,9 +1547,12 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
auto const& arguments = _funCall.arguments();
auto arrayType = dynamic_cast<ArrayType const*>(symbArray->type());
solAssert(arrayType, "");
auto elementType = arrayType->baseType();
smtutil::Expression element = arguments.empty() ?
smt::zeroValue(_funCall.annotation().type) :
expr(*arguments.front());
smt::zeroValue(elementType) :
expr(*arguments.front(), elementType);
smtutil::Expression store = smtutil::Expression::store(
symbArray->elements(),
oldLength,

17
test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol Normal file
View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C {
bytes data;
function g() public {
require(data.length == 0);
data.push("b");
assert(data[0] == "b"); // should hold
assert(data[0] == "c"); // should fail
delete data;
data.push(hex"01");
assert(uint8(data[0]) == 1); // should hold
assert(uint8(data[0]) == 0); // should fail
}
}
// ----
// Warning 6328: (171-193): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (295-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()