Add SMTLogicError exception catches

This commit is contained in:
Leonardo Alt 2020-05-20 12:55:12 +02:00
parent 25de3975ce
commit 0eb067ae4f
2 changed files with 21 additions and 0 deletions

View File

@ -28,6 +28,7 @@
#include <libyul/optimiser/Suite.h>
#include <liblangutil/SourceReferenceFormatter.h>
#include <libevmasm/Instruction.h>
#include <libsmtutil/Exceptions.h>
#include <libsolutil/JSON.h>
#include <libsolutil/Keccak256.h>
#include <libsolutil/CommonData.h>
@ -921,6 +922,16 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
"Yul exception"
));
}
catch (smtutil::SMTLogicError const& _exception)
{
errors.append(formatErrorWithException(
_exception,
false,
"SMTLogicException",
"general",
"SMT logic exception"
));
}
catch (util::Exception const& _exception)
{
errors.append(formatError(

View File

@ -47,6 +47,8 @@
#include <liblangutil/SourceReferenceFormatter.h>
#include <liblangutil/SourceReferenceFormatterHuman.h>
#include <libsmtutil/Exceptions.h>
#include <libsolutil/Common.h>
#include <libsolutil/CommonData.h>
#include <libsolutil/CommonIO.h>
@ -1295,6 +1297,14 @@ bool CommandLineInterface::processInput()
boost::diagnostic_information(_exception);
return false;
}
catch (smtutil::SMTLogicError const& _exception)
{
serr() <<
"SMT logic error during analysis:" <<
endl <<
boost::diagnostic_information(_exception);
return false;
}
catch (Error const& _error)
{
if (_error.type() == Error::Type::DocstringParsingError)