From fb086ea4b4e5501820d582612aeb99c8d2d71966 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Mon, 30 Sep 2024 18:15:56 -0700
Subject: [PATCH] Exclude Charon when running clippy

---
 .github/workflows/format-check.yml |  2 +-
 kani-driver/src/args/mod.rs        | 17 ++++++++---------
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml
index cc13306a4eaf..81253f1a9790 100644
--- a/.github/workflows/format-check.yml
+++ b/.github/workflows/format-check.yml
@@ -47,7 +47,7 @@ jobs:
 
       - name: 'Run Clippy'
         run: |
-          cargo clippy --all -- -D warnings
+          cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings
 
       - name: 'Print Clippy Statistics'
         run: |
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 8c61173bae0e..b32b2e3a52a7 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -636,16 +636,15 @@ impl ValidateArgs for VerificationArgs {
             ));
         }
 
-        if self.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
-            if !self.cbmc_args.is_empty() {
-                return Err(Error::raw(
-                    ErrorKind::ArgumentConflict,
-                    "The `--cbmc-args` argument cannot be used with -Z aeneas.",
-                ));
-            }
-            // TODO: error out for other CBMC-backend-specific arguments
+        // TODO: error out for other CBMC-backend-specific arguments
+        if self.common_args.unstable_features.contains(UnstableFeature::Aeneas)
+            && !self.cbmc_args.is_empty()
+        {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The `--cbmc-args` argument cannot be used with -Z aeneas.",
+            ));
         }
-
         Ok(())
     }
 }