cerc-io/solidity
10
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] additional regression tests

Browse Source
This commit is contained in:
Martin Blicha 2021-01-14 14:01:05 +01:00
parent 504e4c22b2
commit 2ee0f347b9
3 changed files with 29 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata data) external pure returns (uint256[] memory) {
return abi.decode(data, (uint256[]));
}
}
// ----
// Warning 8364: (148-157): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (147-158): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (148-157): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (147-158): Assertion checker does not yet implement type type(uint256[] memory)

9
test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public view {
abi.encode(this.f);
}
}
// ----
// Warning 6031: (86-92): Internal error: Expression undefined for SMT solver.
// Warning 6031: (86-92): Internal error: Expression undefined for SMT solver.

9
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal_2.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(bytes4 sel) public pure {
bytes memory b1 = abi.encodeWithSelector("");
require(sel == "");
bytes memory b2 = abi.encodeWithSelector(sel);
assert(b1.length == b2.length); // should hold
}
}