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

Merge pull request #3020 from ethereum/smt-functioncall

Browse Source 
SMT should not crash on special function calls (typecast)
This commit is contained in:
Alex Beregszaszi 2017-10-05 14:04:16 +01:00 committed by GitHub
commit 8b26d65b62
2 changed files with 36 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolidity/formal/SMTChecker.cpp
View File

@ -234,6 +234,16 @@ void SMTChecker::endVisit(BinaryOperation const& _op)
void SMTChecker::endVisit(FunctionCall const& _funCall) void SMTChecker::endVisit(FunctionCall const& _funCall)
{ {
solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
{
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet implement this expression."
);
return;
}
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments(); std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();

26
test/libsolidity/SMTChecker.cpp
View File

@ -79,6 +79,32 @@ BOOST_AUTO_TEST_CASE(simple_overflow)
CHECK_WARNING(text, "Overflow (resulting value larger than"); CHECK_WARNING(text, "Overflow (resulting value larger than");
} }
BOOST_AUTO_TEST_CASE(warn_on_typecast)
{
string text = R"(
contract C {
function f() public pure returns (uint) {
return uint8(1);
}
}
)";
CHECK_WARNING(text, "Assertion checker does not yet implement this expression.");
}
BOOST_AUTO_TEST_CASE(warn_on_struct)
{
string text = R"(
contract C {
struct A { uint a; uint b; }
function f() public pure returns (A) {
return A({ a: 1, b: 2 });
}
}
)";
/// Multiple warnings, should check for: Assertion checker does not yet implement this expression.
CHECK_WARNING_ALLOW_MULTI(text, "");
}
BOOST_AUTO_TEST_SUITE_END() BOOST_AUTO_TEST_SUITE_END()
} }