solidity/test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol

28 lines
685 B
Solidity
Raw Normal View History

2021-04-08 19:41:35 +00:00
library L {
function pub() public pure returns (uint) {
return 7;
}
function inter() internal pure returns (uint) {
return 8;
}
}
function fu() pure returns (uint, uint) {
return (L.pub(), L.inter());
}
contract C {
function f() public pure {
(uint x, uint y) = fu();
assert(x == 7); // should hold but SMTChecker doesn't implement delegatecall
assert(y == 9); // should fail
}
}
// ====
// SMTEngine: all
2021-08-23 09:30:12 +00:00
// SMTIgnoreCex: yes
2021-04-08 19:41:35 +00:00
// ----
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
2021-08-23 09:30:12 +00:00
// Warning 6328: (284-298): CHC: Assertion violation happens here.
// Warning 6328: (363-377): CHC: Assertion violation happens here.