From 9eda95caf97e22b00204cbd2d6b6be6f497207f2 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 29 Nov 2019 17:20:50 +0100 Subject: [PATCH] [SMTChecker] Fix visit to IndexAccess that has type Type --- libsolidity/formal/SMTEncoder.cpp | 5 +---- .../special/abi_decode_memory_v2.sol | 13 ++++++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b18cf6719..643e88df1 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -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( diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index e469f06ba..eb82932c3 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -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.