Add SMT tests.

This commit is contained in:
chriseth 2017-09-28 10:28:41 +02:00
parent 5ee3ceaef7
commit a1f3046647
4 changed files with 21 additions and 7 deletions

View File

@ -64,9 +64,11 @@ Running the compiler tests
==========================
Solidity includes different types of tests. They are included in the application
called ``soltest``. Some of them require the ``cpp-ethereum`` client in testing mode.
called ``soltest``. Some of them require the ``cpp-ethereum`` client in testing mode,
some others require ``libz3`` to be installed.
To run a subset of the tests that do not require ``cpp-ethereum``, use ``./build/test/soltest -- --no-ipc``.
To disable the z3 tests, use ``./build/test/soltest -- --no-smt`` and
to run a subset of the tests that do not require ``cpp-ethereum``, use ``./build/test/soltest -- --no-ipc``.
For all other tests, you need to install `cpp-ethereum <https://github.com/ethereum/cpp-ethereum/releases/download/solidityTester/eth>`_ and run it in testing mode: ``eth --test -d /tmp/testeth``.

View File

@ -45,6 +45,8 @@ Options::Options()
showMessages = true;
else if (string(suite.argv[i]) == "--no-ipc")
disableIPC = true;
else if (string(suite.argv[i]) == "--no-smt")
disableSMT = true;
if (!disableIPC && ipcPath.empty())
if (auto path = getenv("ETH_TEST_IPC"))

View File

@ -35,6 +35,7 @@ struct Options: boost::noncopyable
bool showMessages = false;
bool optimize = false;
bool disableIPC = false;
bool disableSMT = false;
static Options const& get();

View File

@ -39,6 +39,17 @@
using namespace boost::unit_test;
namespace
{
void removeTestSuite(std::string const& _name)
{
master_test_suite_t& master = framework::master_test_suite();
auto id = master.get(_name);
assert(id != INV_TEST_UNIT_ID);
master.remove(id);
}
}
test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
{
master_test_suite_t& master = framework::master_test_suite();
@ -57,12 +68,10 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
"SolidityEndToEndTest",
"SolidityOptimizer"
})
{
auto id = master.get(suite);
assert(id != INV_TEST_UNIT_ID);
master.remove(id);
}
removeTestSuite(suite);
}
if (dev::test::Options::get().disableSMT)
removeTestSuite("SMTChecker");
return 0;
}