cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #7306 from ethereum/smt_fix_type_expression

Browse Source 
[SMTChecker] Fix index access type type error
This commit is contained in:
Leonardo 2019-08-28 15:54:30 +02:00 committed by GitHub
commit e74b63b6de
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 54 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolidity/formal/SMTEncoder.cpp
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(),

11
test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol Normal file
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)

12
test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol Normal file
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)

12
test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol Normal file
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)

13
test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol Normal file
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)