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

[SMTChecker] Do not warn on "abi" as an identifer

Browse Source 
There is an approprate warning for the function call.
This commit is contained in:
Alex Beregszaszi 2020-09-24 10:32:56 +01:00
parent 79ae043a53
commit 6edfdff187
10 changed files with 52 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -748,6 +748,13 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
defineExpr(_identifier, m_context.state().thisAddress());
m_uninterpretedTerms.insert(&_identifier);
}
// Ignore the builtin abi, it is handled in FunctionCall.
// TODO: ignore MagicType in general (abi, block, msg, tx, type)
else if (auto magicType = dynamic_cast<MagicType const*>(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI)
{
solAssert(_identifier.name() == "abi", "");
return;
}
else
createExpr(_identifier);
}

2
test/libsolidity/smtCheckerTests/complex/MerkleProof.sol
View File

@ -34,7 +34,5 @@ library MerkleProof {
}
// ----
// Warning 8364: (988-991): Assertion checker does not yet implement type abi
// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call.
// Warning 8364: (1175-1178): Assertion checker does not yet implement type abi
// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -83,7 +83,6 @@ contract InternalCall {
// Warning 2018: (1144-1206): Function state mutability can be restricted to pure
// Warning 2018: (1212-1274): Function state mutability can be restricted to pure
// Warning 2018: (1280-1342): Function state mutability can be restricted to pure
// Warning 8364: (771-774): Assertion checker does not yet implement type abi
// Warning 5084: (782-813): Type conversion is not yet fully supported and might yield false positives.
// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
// Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol
View File

@ -5,7 +5,5 @@ contract C {
}
}
// ----
// Warning 8364: (162-165): Assertion checker does not yet implement type abi
// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call.
// Warning 8364: (178-181): Assertion checker does not yet implement type abi
// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call.

17
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol
View File

@ -2,14 +2,13 @@ pragma experimental SMTChecker;
pragma experimental "ABIEncoderV2";
contract C {
struct S { uint x; uint[] b; }
function f() public pure returns (S memory, bytes memory, uint[][2] memory) {
return abi.decode("abc", (S, bytes, uint[][2]));
}
struct S { uint x; uint[] b; }
function f() public pure returns (S memory, bytes memory, uint[][2] memory) {
return abi.decode("abc", (S, bytes, uint[][2]));
}
}
// ----
// Warning 8364: (206-209): Assertion checker does not yet implement type abi
// Warning 8364: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 8364: (235-241): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (235-244): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 4588: (206-246): Assertion checker does not yet implement this type of function call.
// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call.

24
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol
View File

@ -2,18 +2,16 @@ pragma experimental SMTChecker;
pragma experimental "ABIEncoderV2";
contract C {
function f() public pure {
(uint x1, bool b1) = abi.decode("abc", (uint, bool));
(uint x2, bool b2) = abi.decode("abc", (uint, bool));
// False positive until abi.* are implemented as uninterpreted functions.
assert(x1 == x2);
}
function f() public pure {
(uint x1, bool b1) = abi.decode("abc", (uint, bool));
(uint x2, bool b2) = abi.decode("abc", (uint, bool));
// False positive until abi.* are implemented as uninterpreted functions.
assert(x1 == x2);
}
}
// ----
// Warning 2072: (125-132): Unused local variable.
// Warning 2072: (183-190): Unused local variable.
// Warning 6328: (303-319): Assertion violation happens here.
// Warning 8364: (136-139): Assertion checker does not yet implement type abi
// Warning 4588: (136-167): Assertion checker does not yet implement this type of function call.
// Warning 8364: (194-197): Assertion checker does not yet implement type abi
// Warning 4588: (194-225): Assertion checker does not yet implement this type of function call.
// Warning 2072: (122-129): Unused local variable.
// Warning 2072: (178-185): Unused local variable.
// Warning 6328: (300-316): Assertion violation happens here.
// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call.
// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call.

37
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -1,24 +1,21 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
(uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C));
(uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C));
// False positive until abi.* are implemented as uninterpreted functions.
assert(a1 == a2);
assert(a1 != a2);
}
function f() public pure {
(uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C));
(uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C));
// False positive until abi.* are implemented as uninterpreted functions.
assert(a1 == a2);
assert(a1 != a2);
}
}
// ----
// Warning 2072: (88-98): Unused local variable.
// Warning 2072: (100-104): Unused local variable.
// Warning 2072: (161-171): Unused local variable.
// Warning 2072: (173-177): Unused local variable.
// Warning 6328: (296-312): Assertion violation happens here.
// Warning 6328: (315-331): Assertion violation happens here.
// Warning 8364: (108-111): Assertion checker does not yet implement type abi
// Warning 8364: (142-143): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (108-145): Assertion checker does not yet implement this type of function call.
// Warning 8364: (181-184): Assertion checker does not yet implement type abi
// Warning 8364: (215-216): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (181-218): Assertion checker does not yet implement this type of function call.
// Warning 2072: (85-95): Unused local variable.
// Warning 2072: (97-101): Unused local variable.
// Warning 2072: (156-166): Unused local variable.
// Warning 2072: (168-172): Unused local variable.
// Warning 6328: (293-309): Assertion violation happens here.
// Warning 6328: (313-329): Assertion violation happens here.
// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call.
// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call.

9
test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata data) external pure returns (bytes memory) {
return abi.encode(bytes(data[:32]));
}
}
// ----
// Warning 2923: (143-152): Assertion checker does not yet implement this expression.
// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol
View File

@ -7,4 +7,3 @@ contract K {
}
// ----
// Warning 6133: (76-91): Statement has no effect.
// Warning 8364: (77-80): Assertion checker does not yet implement type abi

1
test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol
View File

@ -7,4 +7,3 @@ contract K {
}
// ----
// Warning 6133: (76-92): Statement has no effect.
// Warning 8364: (77-80): Assertion checker does not yet implement type abi