Merge pull request #5248 from thk123/dont-run-failed-tests

Don't run failed unit tests by default

Author: Thomas Kiley

.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

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:

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:

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\**\*'

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:

jbmc/unit/CMakeLists.txt

@@ -36,4 +36,11 @@ add_test(
     COMMAND $<TARGET_FILE:java-unit>
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
+
+add_test(
+    NAME java-unit-xfail
+    COMMAND $<TARGET_FILE:java-unit> "[!shouldfail]"
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
 set_tests_properties(java-unit PROPERTIES LABELS "CORE;CBMC")

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}
 
 
 ###############################################################################

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",

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) {

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);

unit/CMakeLists.txt

@@ -65,4 +65,11 @@ add_test(
     COMMAND $<TARGET_FILE:unit>
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
+
+add_test(
+    NAME unit-xfail
+    COMMAND $<TARGET_FILE:unit> "[!shouldfail]"
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
 set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC")

unit/Makefile

@@ -207,9 +207,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}
 
 
 ###############################################################################

unit/testing-utils/use_catch.h

@@ -36,4 +36,7 @@ Author: Michael Tautschnig
 #include <util/pragma_pop.def>
 #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

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 <util/expr.h>
 
-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(...))")
   {