Add nooptions label to smt checks.

This commit is contained in:
Daniel Kirchner 2020-07-10 11:22:57 +02:00
parent d1ea33bcca
commit c8f25142a7
5 changed files with 16 additions and 9 deletions

View File

@ -46,6 +46,7 @@ struct Testsuite
bool smt;
bool needsVM;
TestCase::TestCaseCreator testCaseCreator;
std::vector<std::string> labels{};
};
@ -64,8 +65,8 @@ Testsuite const g_interactiveTestsuites[] = {
{"Semantic", "libsolidity", "semanticTests", false, true, &SemanticTest::create},
{"JSON AST", "libsolidity", "ASTJSON", false, false, &ASTJSONTest::create},
{"JSON ABI", "libsolidity", "ABIJson", false, false, &ABIJsonTest::create},
{"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SMTCheckerTest::create},
{"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerJSONTest::create},
{"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SMTCheckerTest::create, {"nooptions"}},
{"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerJSONTest::create, {"nooptions"}},
{"Gas Estimates", "libsolidity", "gasTests", false, false, &GasTest::create}
};

View File

@ -65,6 +65,7 @@ int registerTests(
boost::filesystem::path const& _basepath,
boost::filesystem::path const& _path,
bool _enforceViaYul,
vector<string> const& _labels,
TestCase::TestCaseCreator _testCaseCreator
)
{
@ -83,6 +84,7 @@ int registerTests(
*sub_suite,
_basepath, _path / entry.path().filename(),
_enforceViaYul,
_labels,
_testCaseCreator
);
_suite.add(sub_suite);
@ -95,7 +97,7 @@ int registerTests(
static vector<unique_ptr<string const>> filenames;
filenames.emplace_back(make_unique<string>(_path.string()));
_suite.add(make_test_case(
auto test_case = make_test_case(
[config, _testCaseCreator]
{
BOOST_REQUIRE_NO_THROW({
@ -125,7 +127,10 @@ int registerTests(
_path.stem().string(),
*filenames.back(),
0
));
);
for (auto const& _label: _labels)
test_case->add_label(_label);
_suite.add(test_case);
numTestsAdded = 1;
}
return numTestsAdded;
@ -174,6 +179,7 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
options.testPath / ts.path,
ts.subpath,
options.enforceViaYul,
ts.labels,
ts.testCaseCreator
) > 0, std::string("no ") + ts.title + " tests found");
}

View File

@ -55,7 +55,7 @@ protected:
BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
BOOST_AUTO_TEST_CASE(import_base)
BOOST_AUTO_TEST_CASE(import_base, *boost::unit_test::label("no_options"))
{
CompilerStack c;
c.setSources({
@ -97,7 +97,7 @@ BOOST_AUTO_TEST_CASE(import_base)
BOOST_CHECK_EQUAL(asserts, 1);
}
BOOST_AUTO_TEST_CASE(import_library)
BOOST_AUTO_TEST_CASE(import_library, *boost::unit_test::label("no_options"))
{
CompilerStack c;
c.setSources({

View File

@ -26,7 +26,7 @@ using namespace solidity::langutil;
using namespace solidity::frontend;
using namespace solidity::frontend::test;
SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion): SyntaxTest(_filename, _evmVersion)
SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{})
{
auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
if (choice == "any")

View File

@ -31,9 +31,9 @@ class SMTCheckerTest: public SyntaxTest
public:
static std::unique_ptr<TestCase> create(Config const& _config)
{
return std::make_unique<SMTCheckerTest>(_config.filename, _config.evmVersion);
return std::make_unique<SMTCheckerTest>(_config.filename);
}
SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
SMTCheckerTest(std::string const& _filename);
TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;