Remove empty assertion messages in a fews places

This commit is contained in:
Kamil Śliwak 2022-06-01 20:15:02 +02:00
parent 539e139555
commit e19e6ad806
3 changed files with 9 additions and 10 deletions

View File

@ -278,7 +278,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments); return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
} }
smtAssert(false, ""); smtAssert(false);
} }
catch (CVC4::TypeCheckingException const& _e) catch (CVC4::TypeCheckingException const& _e)
{ {
@ -289,7 +289,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
smtAssert(false, _e.what()); smtAssert(false, _e.what());
} }
smtAssert(false, ""); smtAssert(false);
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794) // FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
throw exception(); throw exception();

View File

@ -264,14 +264,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return constructor(args); return constructor(args);
} }
smtAssert(false, ""); smtAssert(false);
} }
catch (z3::exception const& _e) catch (z3::exception const& _e)
{ {
smtAssert(false, _e.msg()); smtAssert(false, _e.msg());
} }
smtAssert(false, ""); smtAssert(false);
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794) // FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
throw exception(); throw exception();
@ -382,7 +382,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
) )
return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort())); return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
smtAssert(false, ""); smtAssert(false);
// FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794) // FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794)
throw exception(); throw exception();

View File

@ -1637,7 +1637,7 @@ ASTPointer<Statement> Parser::parseSimpleStatement(ASTPointer<ASTString> const&
return parseExpressionStatement(_docString, nodeFactory.createNode<TupleExpression>(components, false)); return parseExpressionStatement(_docString, nodeFactory.createNode<TupleExpression>(components, false));
} }
default: default:
solAssert(false, ""); solAssert(false);
} }
} }
else else
@ -1650,7 +1650,7 @@ ASTPointer<Statement> Parser::parseSimpleStatement(ASTPointer<ASTString> const&
case LookAheadInfo::Expression: case LookAheadInfo::Expression:
return parseExpressionStatement(_docString, expressionFromIndexAccessStructure(iap)); return parseExpressionStatement(_docString, expressionFromIndexAccessStructure(iap));
default: default:
solAssert(false, ""); solAssert(false);
} }
} }
@ -1661,9 +1661,8 @@ ASTPointer<Statement> Parser::parseSimpleStatement(ASTPointer<ASTString> const&
bool Parser::IndexAccessedPath::empty() const bool Parser::IndexAccessedPath::empty() const
{ {
if (!indices.empty()) if (!indices.empty())
{ solAssert(!path.empty());
solAssert(!path.empty(), "");
}
return path.empty() && indices.empty(); return path.empty() && indices.empty();
} }