Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm_gtest.h
Go to the documentation of this file.
1#pragma once
2
3#pragma clang diagnostic push
4#pragma clang diagnostic ignored "-Wundef"
5#include <gtest/gtest.h>
6#pragma clang diagnostic pop
7
8#include <boost/optional/optional_io.hpp>
9
13
14#define STORM_SILENT_ASSERT_THROW(statement, expected_exception) \
15 storm::test::disableOutput(); \
16 ASSERT_THROW(statement, expected_exception); \
17 storm::test::enableErrorOutput()
18
19#define STORM_SILENT_EXPECT_THROW(statement, expected_exception) \
20 storm::test::disableOutput(); \
21 EXPECT_THROW(statement, expected_exception); \
22 storm::test::enableErrorOutput()
23
24// Annotate test cases that are too expensive to run in every CI run (identified via profiling) with STORM_EXPENSIVE_*.
25// These macros expand to gtest's DISABLED_ prefix, so the tests are skipped by default and can be re-enabled at run time
26// without reconfiguring the build, either via --gtest_also_run_disabled_tests or the GTEST_ALSO_RUN_DISABLED_TESTS=1
27// environment variable.
28#define STORM_EXPENSIVE_TEST(test_suite_name, test_name) TEST(test_suite_name, DISABLED_##test_name)
29#define STORM_EXPENSIVE_TEST_F(test_suite_name, test_name) TEST_F(test_suite_name, DISABLED_##test_name)
30#define STORM_EXPENSIVE_TEST_P(test_suite_name, test_name) TEST_P(test_suite_name, DISABLED_##test_name)
31#define STORM_EXPENSIVE_TYPED_TEST(test_suite_name, test_name) TYPED_TEST(test_suite_name, DISABLED_##test_name)
32
33namespace testing {
34namespace internal {
35
36GTEST_API_ AssertionResult DoubleNearPredFormat(const char* expr1, const char* expr2, const char* abs_error_expr, storm::RationalNumber val1,
37 storm::RationalNumber val2, storm::RationalNumber abs_error);
38} // namespace internal
39} // namespace testing
40
41namespace storm {
42namespace test {
43extern bool noGurobi;
44
45void initialize(int* argc, char** argv);
46
47inline void enableErrorOutput() {
48 // Only decrease the log level
49 if (storm::utility::getLogLevel() > l3pp::LogLevel::ERR) {
50 storm::utility::setLogLevel(l3pp::LogLevel::ERR);
51 }
52}
53
54inline void disableOutput() {
55 storm::utility::setLogLevel(l3pp::LogLevel::OFF);
56}
57
58// Check for valid Gurobi license
60
61// Some tests have to be skipped for specific z3 versions because of a bug that was present in z3.
62#ifdef STORM_HAVE_Z3
63bool z3AtLeastVersion(unsigned expectedMajor, unsigned expectedMinor, unsigned expectedBuildNumber);
64#endif
65} // namespace test
66} // namespace storm
bool testGurobiLicense()
void disableOutput()
Definition storm_gtest.h:54
void enableErrorOutput()
Definition storm_gtest.h:47
void initialize(int *argc, char **argv)
void setLogLevel(l3pp::LogLevel level)
Set the global log level.
l3pp::LogLevel getLogLevel()
Gets the global log level.
GTEST_API_ AssertionResult DoubleNearPredFormat(const char *expr1, const char *expr2, const char *abs_error_expr, storm::RationalNumber val1, storm::RationalNumber val2, storm::RationalNumber abs_error)