[SMTChecker] Fix index access type type error

This commit is contained in:
Leonardo Alt 2019-08-27 16:39:19 +02:00
parent a54d69b8ef
commit 214e5c6369
5 changed files with 54 additions and 0 deletions

View File

@ -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(),

View File

@ -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)

View File

@ -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)

View File

@ -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)

View File

@ -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)