[SMTChecker] Fix visit to IndexAccess that has type Type

This commit is contained in:
Leonardo Alt 2019-11-29 17:20:50 +01:00
parent 27097b3eca
commit 9eda95caf9
2 changed files with 9 additions and 9 deletions

View File

@ -899,11 +899,8 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
return;
}
if (!_indexAccess.indexExpression())
{
solAssert(_indexAccess.annotation().type->category() == Type::Category::TypeType, "");
if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
return;
}
solAssert(array, "");
defineExpr(_indexAccess, smt::Expression::select(

View File

@ -3,13 +3,16 @@ pragma experimental "ABIEncoderV2";
contract C {
struct S { uint x; uint[] b; }
function f() public pure returns (S memory, bytes memory) {
return abi.decode("abc", (S, bytes));
function f() public pure returns (S memory, bytes memory, uint[][2] memory) {
return abi.decode("abc", (S, bytes, uint[][2]));
}
}
// ----
// Warning: (32-67): Experimental features are turned on. Do not use experimental features on live deployments.
// Warning: (151-159): Assertion checker does not yet support the type of this variable.
// Warning: (188-191): Assertion checker does not yet implement type abi
// Warning: (207-208): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (188-217): Assertion checker does not yet implement this type of function call.
// Warning: (206-209): Assertion checker does not yet implement type abi
// Warning: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (235-241): Assertion checker does not yet implement type type(uint256[] memory)
// Warning: (235-241): Assertion checker does not yet implement this expression.
// Warning: (235-244): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning: (206-246): Assertion checker does not yet implement this type of function call.