Fix -Werror issues with clang and use clang for debug-cln build. (#6004)

This fixes some issues that break the nightly ASAN builds with clang.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 753872ae1f18350e2760ead5fd3063f33322aa35..fd6b65998bf6b94fc709c4da22eadf4fd16fb221 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -10,7 +10,7 @@ jobs:
           production,
           production-clang,
           debug,
-          debug-cln
+          debug-cln-clang
         ]
 
         exclude:
@@ -18,7 +18,7 @@ jobs:
             os: macos-latest
           - name: debug
             os: macos-latest
-          - name: debug-cln
+          - name: debug-cln-clang
             os: macos-latest
 
         include:
@@ -43,9 +43,10 @@ jobs:
             os: ubuntu-latest
             exclude_regress: 1-4
 
-          - name: debug-cln
+          - name: debug-cln-clang
             config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs --poly
-            cache-key: debug-cln
+            cache-key: debug-cln-clang
+            env: CC=clang CXX=clang++
             os: ubuntu-latest
             exclude_regress: 1-4
 

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index a6291178b2e7a0f8848eec8d5142e5d5204a39c4..46ff346e04e173ceb1585e41df59ed4345280dff 100644 (file)
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -57,6 +57,11 @@ macro(cvc4_add_unit_test is_white name output_dir)
   if(${is_white})
     target_compile_options(${name} PRIVATE -fno-access-control)
   endif()
+  # Disable the Wunused-comparison warnings for the unit tests.
+  check_cxx_compiler_flag("-Wno-unused-comparison" HAVE_FLAGWno_unused_comparison)
+  if(HAVE_FLAGWno_unused_comparison)
+    target_compile_options(${name} PRIVATE -Wno-unused-comparison)
+  endif()
   add_dependencies(build-units ${name})
   # Generate into bin/test/unit/<output_dir>.
   set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
@@ -125,7 +130,16 @@ macro(cvc4_add_cxx_unit_test is_white name output_dir)
   endif()
   # Disable the Wsuggest-override warnings for the unit tests. CxxTest generates
   # code that does not properly add the override keyword to runTest().
-  target_compile_options(${name} PRIVATE -Wno-suggest-override)
+  check_cxx_compiler_flag("-Wno-suggest-override" HAVE_FLAGWno_suggest_override)
+  if(HAVE_FLAGWno_suggest_override)
+    target_compile_options(${name} PRIVATE -Wno-suggest-override)
+  endif()
+  # Disable the Wunused-comparison warnings for the unit tests.
+  check_cxx_compiler_flag("-Wno-unused-comparison" HAVE_FLAGWno_unused_comparison)
+  if(HAVE_FLAGWno_unused_comparison)
+    target_compile_options(${name} PRIVATE -Wno-unused-comparison)
+  endif()
+
   add_dependencies(build-units ${name})
   # Generate into bin/test/unit/<output_dir>.
   set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 4b6c1a0643ae5924a793bf10ee9d7f0b26508e92..5ac316612337a0aec536a549939d1e833e5c4e33 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -108,7 +108,7 @@ class DummyTheory : public Theory {
     d_theoryState = &d_state;
   }
 
-  TheoryRewriter* getTheoryRewriter() { return nullptr; }
+  TheoryRewriter* getTheoryRewriter() override { return nullptr; }
 
   void registerTerm(TNode n) {
     // check that we registerTerm() a term only once