From 214e5c6369d4c3c0994b689af249f665905a3ebe Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 27 Aug 2019 16:39:19 +0200 Subject: [PATCH] [SMTChecker] Fix index access type type error --- libsolidity/formal/SMTEncoder.cpp | 6 ++++++ .../types/type_expression_array_2d.sol | 11 +++++++++++ .../types/type_expression_array_3d.sol | 12 ++++++++++++ .../types/type_expression_tuple_array_2d.sol | 12 ++++++++++++ .../types/type_expression_tuple_array_3d.sol | 13 +++++++++++++ 5 files changed, 54 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol create mode 100644 test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol create mode 100644 test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol create mode 100644 test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 85ec5e776..421bfb3b6 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -748,6 +748,12 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) return; } + if (!_indexAccess.indexExpression()) + { + solAssert(_indexAccess.annotation().type->category() == Type::Category::TypeType, ""); + return; + } + solAssert(array, ""); defineExpr(_indexAccess, smt::Expression::select( array->currentValue(), diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol new file mode 100644 index 000000000..f63e6aef3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +contract C { + +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 new file mode 100644 index 000000000..2588ee98d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + +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 new file mode 100644 index 000000000..02c2ac056 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + +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 new file mode 100644 index 000000000..893f30581 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + +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)