diff --git a/Changelog.md b/Changelog.md index d50b9f590..af170ed01 100644 --- a/Changelog.md +++ b/Changelog.md @@ -19,6 +19,7 @@ Build System: Bugfixes: * SMTChecker: Fix internal error when using ``abi.decode``. * SMTChecker: Fix internal error when using arrays or mappings of functions. + * SMTChecker: Fix internal error in array of structs type. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 643e88df1..0f04f412b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -869,8 +869,11 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) { createExpr(_indexAccess); + if (_indexAccess.annotation().type->category() == Type::Category::TypeType) + return; + shared_ptr array; - if (auto const& id = dynamic_cast(&_indexAccess.baseExpression())) + if (auto const* id = dynamic_cast(&_indexAccess.baseExpression())) { auto varDecl = identifierToVariable(*id); solAssert(varDecl, ""); @@ -885,7 +888,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) return; } } - else if (auto const& innerAccess = dynamic_cast(&_indexAccess.baseExpression())) + else if (auto const* innerAccess = dynamic_cast(&_indexAccess.baseExpression())) { solAssert(m_context.knownExpression(*innerAccess), ""); array = m_context.expression(*innerAccess); @@ -899,9 +902,6 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) return; } - if (_indexAccess.annotation().type->category() == Type::Category::TypeType) - return; - solAssert(array, ""); defineExpr(_indexAccess, smt::Expression::select( array->currentValue(), diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index eb82932c3..154939913 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -13,6 +13,5 @@ contract C { // 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. diff --git a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol new file mode 100644 index 000000000..f4d1299e9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; +contract test { + struct s { uint a; uint b;} + function f() pure public returns (byte) { + s; + s(1,2); + s[7]; + uint; + uint[7]; + } +} +// ---- +// Warning: (125-126): Statement has no effect. +// Warning: (130-136): Statement has no effect. +// Warning: (140-144): Statement has no effect. +// Warning: (148-152): Statement has no effect. +// Warning: (156-163): Statement has no effect. +// Warning: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer) +// Warning: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer) +// Warning: (130-136): Assertion checker does not yet implement type struct test.s memory +// Warning: (130-136): Assertion checker does not yet implement this expression. +// Warning: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer) +// Warning: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory) +// Warning: (156-163): Assertion checker does not yet implement type type(uint256[7] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol index f63e6aef3..2bd64030d 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol @@ -7,5 +7,4 @@ function f() public pure { int[][]; } // ---- // Warning: (73-80): Statement has no effect. // Warning: (73-78): Assertion checker does not yet implement type type(int256[] memory) -// Warning: (73-78): Assertion checker does not yet implement this expression. // Warning: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol index 2588ee98d..3f0967caf 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol @@ -7,6 +7,5 @@ function f() public pure { int[][][]; } // ---- // Warning: (73-82): Statement has no effect. // Warning: (73-78): Assertion checker does not yet implement type type(int256[] memory) -// Warning: (73-78): Assertion checker does not yet implement this expression. // Warning: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory) // Warning: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol index 02c2ac056..e648b5d6d 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol @@ -7,6 +7,5 @@ function f() public pure { (int[][]); } // ---- // Warning: (73-82): Statement has no effect. // Warning: (74-79): Assertion checker does not yet implement type type(int256[] memory) -// Warning: (74-79): Assertion checker does not yet implement this expression. // Warning: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory) // Warning: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol index 893f30581..2d66a3bb2 100644 --- a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol @@ -7,7 +7,6 @@ function f() public pure { (int[][][]); } // ---- // Warning: (73-84): Statement has no effect. // Warning: (74-79): Assertion checker does not yet implement type type(int256[] memory) -// Warning: (74-79): Assertion checker does not yet implement this expression. // Warning: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory) // Warning: (74-83): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory) // Warning: (73-84): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)