From 92945908fad99e379056199654a113fc2b2ac648 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Fri, 27 Sep 2024 15:43:41 -0700
Subject: [PATCH] Error out if CBMC-specific options are used with Aeneas
 backend

---
 kani-driver/src/args/mod.rs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 7e2704dd6b04..7dbfffbdad7c 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -636,6 +636,16 @@ 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
+        }
+
         Ok(())
     }
 }
@@ -926,4 +936,11 @@ mod tests {
         check_invalid_args("kani input.rs --package foo".split_whitespace());
         check_invalid_args("kani input.rs --exclude bar --workspace".split_whitespace());
     }
+
+    #[test]
+    fn check_cbmc_args_aeneas_backend() {
+        let args = "kani input.rs -Z aeneas --enable-unstable --cbmc-args --object-bits 10".split_whitespace();
+        let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
+        assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
+    }
 }