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

Fix internal error when using array slices

Browse Source
This commit is contained in:
Leonardo Alt 2020-04-22 18:54:38 +02:00
parent 6d98b907ef
commit cfe3686116
4 changed files with 37 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix internal error when fixed points are used.
* SMTChecker: Fix internal error when using array slices.
* Type Checker: Disallow ``virtual`` and ``override`` for constructors.
* Type Checker: Fix several internal errors by performing size and recursiveness checks of types before the full type checking.
* Type Checker: Perform recursiveness check on structs declared at the file level.

13
libsolidity/formal/SymbolicTypes.cpp
View File

@ -69,8 +69,14 @@ SortPointer smtSort(frontend::Type const& _type)
}
else
{
solAssert(isArray(_type.category()), "");
auto arrayType = dynamic_cast<frontend::ArrayType const*>(&_type);
frontend::ArrayType const* arrayType = nullptr;
if (auto const* arr = dynamic_cast<frontend::ArrayType const*>(&_type))
arrayType = arr;
else if (auto const* slice = dynamic_cast<frontend::ArraySliceType const*>(&_type))
arrayType = &slice->arrayType();
else
solAssert(false, "");
solAssert(arrayType, "");
return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
}
@ -297,7 +303,8 @@ bool isMapping(frontend::Type::Category _category)
bool isArray(frontend::Type::Category _category)
{
return _category == frontend::Type::Category::Array ||
_category == frontend::Type::Category::StringLiteral;
_category == frontend::Type::Category::StringLiteral ||
_category == frontend::Type::Category::ArraySlice;
}
bool isTuple(frontend::Type::Category _category)

13
test/libsolidity/smtCheckerTests/operators/slices_1.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata x) external pure {
x[:18726387213];
x[18726387213:];
x[18726387213:111111111111111111];
}
}
// ----
// Warning: (94-109): Assertion checker does not yet implement this expression.
// Warning: (113-128): Assertion checker does not yet implement this expression.
// Warning: (132-165): Assertion checker does not yet implement this expression.

13
test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata x) external pure {
bytes(x[:18726387213]);
bytes(x[18726387213:]);
bytes(x[18726387213:111111111111111111]);
}
}
// ----
// Warning: (100-115): Assertion checker does not yet implement this expression.
// Warning: (126-141): Assertion checker does not yet implement this expression.
// Warning: (152-185): Assertion checker does not yet implement this expression.