mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #9377 from ethereum/smtNoOptions
Add nooptions label to smt checks.
This commit is contained in:
commit
b7b3411464
@ -46,6 +46,7 @@ struct Testsuite
|
|||||||
bool smt;
|
bool smt;
|
||||||
bool needsVM;
|
bool needsVM;
|
||||||
TestCase::TestCaseCreator testCaseCreator;
|
TestCase::TestCaseCreator testCaseCreator;
|
||||||
|
std::vector<std::string> labels{};
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
@ -64,8 +65,8 @@ Testsuite const g_interactiveTestsuites[] = {
|
|||||||
{"Semantic", "libsolidity", "semanticTests", false, true, &SemanticTest::create},
|
{"Semantic", "libsolidity", "semanticTests", false, true, &SemanticTest::create},
|
||||||
{"JSON AST", "libsolidity", "ASTJSON", false, false, &ASTJSONTest::create},
|
{"JSON AST", "libsolidity", "ASTJSON", false, false, &ASTJSONTest::create},
|
||||||
{"JSON ABI", "libsolidity", "ABIJson", false, false, &ABIJsonTest::create},
|
{"JSON ABI", "libsolidity", "ABIJson", false, false, &ABIJsonTest::create},
|
||||||
{"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SMTCheckerTest::create},
|
{"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SMTCheckerTest::create, {"nooptions"}},
|
||||||
{"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerJSONTest::create},
|
{"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerJSONTest::create, {"nooptions"}},
|
||||||
{"Gas Estimates", "libsolidity", "gasTests", false, false, &GasTest::create}
|
{"Gas Estimates", "libsolidity", "gasTests", false, false, &GasTest::create}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -65,6 +65,7 @@ int registerTests(
|
|||||||
boost::filesystem::path const& _basepath,
|
boost::filesystem::path const& _basepath,
|
||||||
boost::filesystem::path const& _path,
|
boost::filesystem::path const& _path,
|
||||||
bool _enforceViaYul,
|
bool _enforceViaYul,
|
||||||
|
vector<string> const& _labels,
|
||||||
TestCase::TestCaseCreator _testCaseCreator
|
TestCase::TestCaseCreator _testCaseCreator
|
||||||
)
|
)
|
||||||
{
|
{
|
||||||
@ -83,6 +84,7 @@ int registerTests(
|
|||||||
*sub_suite,
|
*sub_suite,
|
||||||
_basepath, _path / entry.path().filename(),
|
_basepath, _path / entry.path().filename(),
|
||||||
_enforceViaYul,
|
_enforceViaYul,
|
||||||
|
_labels,
|
||||||
_testCaseCreator
|
_testCaseCreator
|
||||||
);
|
);
|
||||||
_suite.add(sub_suite);
|
_suite.add(sub_suite);
|
||||||
@ -95,7 +97,7 @@ int registerTests(
|
|||||||
static vector<unique_ptr<string const>> filenames;
|
static vector<unique_ptr<string const>> filenames;
|
||||||
|
|
||||||
filenames.emplace_back(make_unique<string>(_path.string()));
|
filenames.emplace_back(make_unique<string>(_path.string()));
|
||||||
_suite.add(make_test_case(
|
auto test_case = make_test_case(
|
||||||
[config, _testCaseCreator]
|
[config, _testCaseCreator]
|
||||||
{
|
{
|
||||||
BOOST_REQUIRE_NO_THROW({
|
BOOST_REQUIRE_NO_THROW({
|
||||||
@ -125,7 +127,10 @@ int registerTests(
|
|||||||
_path.stem().string(),
|
_path.stem().string(),
|
||||||
*filenames.back(),
|
*filenames.back(),
|
||||||
0
|
0
|
||||||
));
|
);
|
||||||
|
for (auto const& _label: _labels)
|
||||||
|
test_case->add_label(_label);
|
||||||
|
_suite.add(test_case);
|
||||||
numTestsAdded = 1;
|
numTestsAdded = 1;
|
||||||
}
|
}
|
||||||
return numTestsAdded;
|
return numTestsAdded;
|
||||||
@ -174,6 +179,7 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
|
|||||||
options.testPath / ts.path,
|
options.testPath / ts.path,
|
||||||
ts.subpath,
|
ts.subpath,
|
||||||
options.enforceViaYul,
|
options.enforceViaYul,
|
||||||
|
ts.labels,
|
||||||
ts.testCaseCreator
|
ts.testCaseCreator
|
||||||
) > 0, std::string("no ") + ts.title + " tests found");
|
) > 0, std::string("no ") + ts.title + " tests found");
|
||||||
}
|
}
|
||||||
|
@ -55,7 +55,7 @@ protected:
|
|||||||
|
|
||||||
BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
|
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;
|
CompilerStack c;
|
||||||
c.setSources({
|
c.setSources({
|
||||||
@ -97,7 +97,7 @@ BOOST_AUTO_TEST_CASE(import_base)
|
|||||||
BOOST_CHECK_EQUAL(asserts, 1);
|
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;
|
CompilerStack c;
|
||||||
c.setSources({
|
c.setSources({
|
||||||
|
@ -26,7 +26,7 @@ using namespace solidity::langutil;
|
|||||||
using namespace solidity::frontend;
|
using namespace solidity::frontend;
|
||||||
using namespace solidity::frontend::test;
|
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");
|
auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
|
||||||
if (choice == "any")
|
if (choice == "any")
|
||||||
|
@ -31,9 +31,9 @@ class SMTCheckerTest: public SyntaxTest
|
|||||||
public:
|
public:
|
||||||
static std::unique_ptr<TestCase> create(Config const& _config)
|
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;
|
TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user