diff --git a/.travis.yml b/.travis.yml index b77d06bdd95..96eaf09200f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -243,7 +243,7 @@ jobs: - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On' - git submodule update --init --recursive - cmake --build build -- -j4 - script: (cd build; ctest -V -L CORE -j2) + script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2) # cmake build using clang++-6 - stage: Test different OS/CXX/Flags @@ -280,7 +280,7 @@ jobs: - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On' - git submodule update --init --recursive - cmake --build build -- -j4 - script: (cd build; ctest -V -L CORE -j2) + script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2) # cmake build on OSX, using default clang - stage: Test different OS/CXX/Flags @@ -300,7 +300,7 @@ jobs: - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64' - git submodule update --init --recursive - cmake --build build -- -j4 - script: (cd build; ctest -V -L CORE -j2) + script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2) # Run Coverity @@ -355,9 +355,13 @@ script: - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2 - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 - make -C unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C unit test - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2 - make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 - make -C jbmc/unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C jbmc/unit test before_cache: - ccache -s diff --git a/buildspec-linux-clang.yml b/buildspec-linux-clang.yml index 5ef62595ad8..ec78098a47f 100644 --- a/buildspec-linux-clang.yml +++ b/buildspec-linux-clang.yml @@ -27,10 +27,14 @@ phases: post_build: commands: - make -C unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C unit test - make -C regression test CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' - make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - make -C jbmc/unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C jbmc/unit test - make -C jbmc/regression test - echo Build completed on `date` cache: diff --git a/buildspec-linux-cmake-gcc.yml b/buildspec-linux-cmake-gcc.yml index d475c985ea2..9f4d176571e 100644 --- a/buildspec-linux-cmake-gcc.yml +++ b/buildspec-linux-cmake-gcc.yml @@ -22,6 +22,7 @@ phases: post_build: commands: - cd build; ctest -V -L CORE -j2 + - cd build; ctest -V -R unit-xfail -j2 - echo Build completed on `date` cache: paths: diff --git a/buildspec-windows.yml b/buildspec-windows.yml index c98fdfe002e..47e8dc3c31c 100644 --- a/buildspec-windows.yml +++ b/buildspec-windows.yml @@ -57,6 +57,10 @@ phases: $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" ' + - | + $env:Path = "C:\tools\cygwin\bin;$env:Path" + cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C unit test BUILD_ENV=MSVC" ' + - | $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC" ' @@ -65,6 +69,10 @@ phases: $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" ' + - | + $env:Path = "C:\tools\cygwin\bin;$env:Path" + cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C jbmc/unit test BUILD_ENV=MSVC" ' + cache: paths: - 'c:\clcache\**\*' diff --git a/buildspec.yml b/buildspec.yml index 62fcdfd0428..3348cb54515 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -26,10 +26,14 @@ phases: post_build: commands: - make -C unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C unit test - make -C regression test - make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - make -C jbmc/unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C jbmc/unit test - make -C jbmc/regression test - echo Build completed on `date` cache: diff --git a/jbmc/unit/CMakeLists.txt b/jbmc/unit/CMakeLists.txt index 6ba62de4903..781e39b66ac 100644 --- a/jbmc/unit/CMakeLists.txt +++ b/jbmc/unit/CMakeLists.txt @@ -36,4 +36,11 @@ add_test( COMMAND $ WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} ) + +add_test( + NAME java-unit-xfail + COMMAND $ "[!shouldfail]" + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} +) + set_tests_properties(java-unit PROPERTIES LABELS "CORE;CBMC") diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index dd03b3266e4..d18567da013 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -144,9 +144,10 @@ all: $(CATCH_TEST) clean: java-testing-utils-clean test: $(CATCH_TEST) - if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ - ./$(CATCH_TEST) -l ; fi - ./$(CATCH_TEST) + # Include hidden tests by specifying "*,[.]" for tests to count + if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ + ./$(CATCH_TEST) "*,[.]" -l ; fi + ./$(CATCH_TEST) ${TAGS} ############################################################################### diff --git a/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp b/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp index c5fba3cf4c3..c5dbcf2cc0d 100644 --- a/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp +++ b/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp @@ -12,7 +12,7 @@ Author: Diffblue Limited. SCENARIO( "Lazy load lambda methods", - "[core][java_bytecode][ci_lazy_methods][lambdas][!mayfail]") + "[core][java_bytecode][ci_lazy_methods][lambdas]") { GIVEN("A class with some locally declared lambdas") { @@ -192,7 +192,7 @@ SCENARIO( SCENARIO( "Lazy load lambda methods in seperate class", - "[core][java_bytecode][ci_lazy_methods][lambdas][!mayfail]") + "[core][java_bytecode][ci_lazy_methods][lambdas]") { const symbol_tablet symbol_table = load_java_class_lazy( "ExternalLambdaAccessor", diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp index bc0846681f2..a63f32a0c7e 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp @@ -188,7 +188,7 @@ void validate_local_variable_lambda_assignment( SCENARIO( "Converting invokedynamic with a local lambda", "[core]" - "[lambdas][java_bytecode][java_bytecode_convert_method][!mayfail]") + "[lambdas][java_bytecode][java_bytecode_convert_method]" XFAIL) { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { @@ -380,7 +380,7 @@ void validate_member_variable_lambda_assignment( SCENARIO( "Converting invokedynamic with a member lambda", "[core]" - "[lamdba][java_bytecode][java_bytecode_convert_method][!mayfail]") + "[lamdba][java_bytecode][java_bytecode_convert_method]" XFAIL) { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { @@ -548,7 +548,7 @@ void validate_static_member_variable_lambda_assignment( SCENARIO( "Converting invokedynamic with a static member lambda", "[core]" - "[lamdba][java_bytecode][java_bytecode_convert_method][!mayfail]") + "[lamdba][java_bytecode][java_bytecode_convert_method]" XFAIL) { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp index 6f1ec9f1ca8..cdcfe9129c2 100644 --- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp @@ -172,10 +172,9 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) return solver(); } -// The [!mayfail] tag allows tests to fail while reporting the failure SCENARIO( "instantiate_not_contains", - "[!mayfail][core][solvers][refinement][string_constraint_instantiation]") + "[core][solvers][refinement][string_constraint_instantiation]" XFAIL) { // For printing expression register_language(new_java_bytecode_language); diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 6a765e74e95..6372702081a 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -65,4 +65,11 @@ add_test( COMMAND $ WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} ) + +add_test( + NAME unit-xfail + COMMAND $ "[!shouldfail]" + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} +) + set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC") diff --git a/unit/Makefile b/unit/Makefile index ccbe365b11f..dbabd7da465 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -204,9 +204,10 @@ all: $(CATCH_TEST) clean: testing-utils-clean test: $(CATCH_TEST) - if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ - ./$(CATCH_TEST) -l ; fi - ./$(CATCH_TEST) + # Include hidden tests by specifying "*,[.]" for tests to count + if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ + ./$(CATCH_TEST) "*,[.]" -l ; fi + ./$(CATCH_TEST) ${TAGS} ############################################################################### diff --git a/unit/testing-utils/use_catch.h b/unit/testing-utils/use_catch.h index 4055b62a8c3..430c8a51c02 100644 --- a/unit/testing-utils/use_catch.h +++ b/unit/testing-utils/use_catch.h @@ -36,4 +36,7 @@ Author: Michael Tautschnig #include #endif +/// Add to the end of test tags to mark a test that is expected to fail +#define XFAIL "[.][!shouldfail]" + #endif // CPROVER_TESTING_UTILS_USE_CATCH_H diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp index 92536974420..aebbed6b5fa 100644 --- a/unit/util/irep_sharing.cpp +++ b/unit/util/irep_sharing.cpp @@ -9,7 +9,7 @@ #ifdef SHARING -SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]") +SCENARIO("irept_sharing_trade_offs", "[core][utils][irept]" XFAIL) { GIVEN("An irept created with move_to_sub") { @@ -116,7 +116,7 @@ SCENARIO("irept_sharing", "[core][utils][irept]") #include -SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]") +SCENARIO("exprt_sharing_trade_offs", "[core][utils][exprt]" XFAIL) { GIVEN("An expression created with add_to_operands(std::move(...))") {