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

Do not run smtCheckerTestsJSON if no solver available

Browse Source
This commit is contained in:
Leonardo Alt 2020-03-10 13:41:10 +01:00
parent 1b17815808
commit bcefda747c
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
test/libsolidity/SMTCheckerJSONTest.cpp
View File

@ -17,14 +17,18 @@
#include <test/libsolidity/SMTCheckerJSONTest.h>
#include <test/Common.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/interface/StandardCompiler.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/JSON.h>
#include <boost/algorithm/string.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include <boost/test/unit_test.hpp>
#include <boost/throw_exception.hpp>
#include <fstream>
#include <memory>
#include <stdexcept>
@ -50,6 +54,9 @@ SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVer
!m_smtResponses.isObject()
)
BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
if (ModelChecker::availableSolvers().none())
m_shouldRun = false;
}
TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)