[SMTChecker] Fix require with message

This commit is contained in:
Leonardo Alt 2019-07-01 16:11:29 +02:00
parent 22776cddcd
commit 75663dc91e
3 changed files with 15 additions and 6 deletions

View File

@ -386,7 +386,7 @@ void BMC::visitAssert(FunctionCall const& _funCall)
void BMC::visitRequire(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1, "");
solAssert(args.size() >= 1, "");
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
if (isRootFunction())
addVerificationTarget(

View File

@ -501,16 +501,16 @@ void SMTEncoder::visitAssert(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
addPathImpliedExpression(expr(*args[0]));
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
addPathImpliedExpression(expr(*args.front()));
}
void SMTEncoder::visitRequire(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
addPathImpliedExpression(expr(*args[0]));
solAssert(args.size() >= 1, "");
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
addPathImpliedExpression(expr(*args.front()));
}
void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f(uint a) public pure {
require(a < 10, "Input number is too large.");
assert(a < 20);
}
}
// ----
// Warning: (97-125): Assertion checker does not yet support the type of this literal (literal_string "Input number is too large.").