cerc-io/solidity
16
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] Support events and low-level logs

Browse Source
This commit is contained in:
Alex Beregszaszi 2020-09-12 12:22:03 +01:00 committed by Leonardo Alt
parent b08b76ffca
commit c8c17b693b
4 changed files with 76 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -5,6 +5,7 @@ Language Features:
Compiler Features:
* Export compiler-generated utility sources via standard-json or combined-json.
* SMTChecker: Support events and low-level logs.
* SMTChecker: Support ``revert()``.
* SMTChecker: Support shifts.
* SMTChecker: Support structs.

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -676,6 +676,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ArrayPop:
arrayPop(_funCall);
break;
case FunctionType::Kind::Log0:
case FunctionType::Kind::Log1:
case FunctionType::Kind::Log2:
case FunctionType::Kind::Log3:
case FunctionType::Kind::Log4:
case FunctionType::Kind::Event:
// These can be safely ignored.
break;
default:
m_errorReporter.warning(
4588_error,

28
test/libsolidity/smtCheckerTests/special/event.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
contract C {
event Nudge();
event SomeArgs(uint, uint);
event Caller(address, uint);
function f() payable external {
emit Nudge();
emit SomeArgs(134, 567);
emit Caller(msg.sender, msg.value);
}
function g_data() pure internal returns (uint) {
assert(true);
}
function g() external {
emit SomeArgs(g_data(), g_data());
}
bool x = true;
function h_data() view internal returns (uint) {
assert(x);
}
function h() external {
x = false;
emit SomeArgs(h_data(), h_data());
}
}
// ----
// Warning 6328: (440-449): Assertion violation happens here.

39
test/libsolidity/smtCheckerTests/special/log.sol Normal file
View File

@ -0,0 +1,39 @@
pragma experimental SMTChecker;
contract C {
function f() external {
bytes32 t1 = bytes32(uint256(0x1234));
log0(t1);
log1(t1, t1);
log2(t1, t1, t1);
log3(t1, t1, t1, t1);
log4(t1, t1, t1, t1, t1);
}
function g_data() pure internal returns (bytes32) {
assert(true);
return bytes32(uint256(0x5678));
}
function g() external {
// To test that the function call is actually visited.
log0(g_data());
log1(g_data(), g_data());
log2(g_data(), g_data(), g_data());
log3(g_data(), g_data(), g_data(), g_data());
log4(g_data(), g_data(), g_data(), g_data(), g_data());
}
bool x = true;
function h_data() view internal returns (bytes32) {
assert(x);
}
function h() external {
// To test that the function call is actually visited.
x = false;
log0(h_data());
log1(h_data(), h_data());
log2(h_data(), h_data(), h_data());
log3(h_data(), h_data(), h_data(), h_data());
log4(h_data(), h_data(), h_data(), h_data(), h_data());
}
}
// ----
// Warning 6328: (668-677): Assertion violation happens here.