Address missed comments from rust-lang#2088 (rust-lang#2200)

Author: zhassan-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -469,7 +469,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let invalid_arg_err = |attr: &Attribute| {
             self.tcx.sess.span_err(
                 attr.span,
-                format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `custom=\"<SAT_SOLVER_BINARY>\"`)")
+                format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"<SAT_SOLVER_BINARY>\"`)")
             )
         };
 
@@ -504,8 +504,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
             }
-            MetaItemKind::NameValue(lit) if ident_str == "custom" && lit.kind.is_str() => {
-                Some(CbmcSolver::Custom(lit.token_lit.symbol.to_string()))
+            MetaItemKind::NameValue(lit) if ident_str == "bin" && lit.kind.is_str() => {
+                Some(CbmcSolver::Binary(lit.token_lit.symbol.to_string()))
             }
             _ => {
                 invalid_arg_err(attr);

kani-driver/src/args.rs

@@ -579,18 +579,18 @@ impl TypedValueParser for CbmcSolverValueParser {
         value: &std::ffi::OsStr,
     ) -> Result<Self::Value, clap::error::Error> {
         let value = value.to_str().unwrap();
-        // `value` is one of the possible `CbmcSolver` values or `custom=<binary>`
+        // `value` is one of the possible `CbmcSolver` values or `bin=<binary>`
         let segments: Vec<&str> = value.split('=').collect();
 
         let mut err = clap::Error::new(ErrorKind::InvalidValue).with_cmd(cmd);
         err.insert(ContextKind::InvalidArg, ContextValue::String(arg.unwrap().to_string()));
         err.insert(ContextKind::InvalidValue, ContextValue::String(value.to_string()));
 
         if segments.len() == 2 {
-            if segments[0] != "custom" {
+            if segments[0] != "bin" {
                 return Err(err);
             }
-            return Ok(CbmcSolver::Custom(segments[1].into()));
+            return Ok(CbmcSolver::Binary(segments[1].into()));
         } else if segments.len() == 1 {
             let solver = CbmcSolver::from_str(value);
             return solver.map_err(|_| err);

kani-driver/src/call_cbmc.rs

@@ -213,13 +213,13 @@ impl KaniSession {
                 // Minisat is currently CBMC's default solver, so no need to
                 // pass any arguments
             }
-            CbmcSolver::Custom(custom_solver) => {
+            CbmcSolver::Binary(solver_binary) => {
                 // Check if the specified binary exists in path
-                if which::which(custom_solver).is_err() {
-                    bail!("the specified solver \"{custom_solver}\" was not found in path")
+                if which::which(solver_binary).is_err() {
+                    bail!("the specified solver \"{solver_binary}\" was not found in path")
                 }
                 args.push("--external-sat-solver".into());
-                args.push(custom_solver.into());
+                args.push(solver_binary.into());
             }
         }
         Ok(())

kani_metadata/src/cbmc_solver.rs

@@ -5,7 +5,7 @@ use serde::{Deserialize, Serialize};
 use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 
 /// An enum for CBMC solver options. All variants are handled by Kani, except for
-/// the `Custom` one, which it passes as is to CBMC's `--external-sat-solver`
+/// the `Binary` one, which it passes as is to CBMC's `--external-sat-solver`
 /// option.
 #[derive(
     Debug,
@@ -26,8 +26,8 @@ pub enum CbmcSolver {
     /// MiniSAT (CBMC's default solver)
     Minisat,
 
-    /// A custom solver variant whose argument gets passed to
+    /// A solver binary variant whose argument gets passed to
     /// `--external-sat-solver`. The specified binary must exist in path.
-    #[strum(disabled, serialize = "custom=<SAT_SOLVER_BINARY>")]
-    Custom(String),
+    #[strum(disabled, serialize = "bin=<SAT_SOLVER_BINARY>")]
+    Binary(String),
 }

tests/ui/solver-attribute/invalid/expected

@@ -1,6 +1,6 @@
-error: invalid argument for `#[kani::solver]` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `custom="<SAT_SOLVER_BINARY>"`)\
+error: invalid argument for `#[kani::solver]` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin="<SAT_SOLVER_BINARY>"`)\
 test.rs:\
-  |\
-5 | #[kani::solver(123)]\
-  | ^^^^^^^^^^^^^^^^^^^^
+|\
+| #[kani::solver(123)]\
+| ^^^^^^^^^^^^^^^^^^^^
 error: aborting due to previous error

tests/ui/solver-attribute/multiple-args/expected

@@ -1,6 +1,6 @@
 error: the `#[kani::solver]` attribute expects a single argument. Got 2 arguments.\
 test.rs:\
-  |\
-5 | #[kani::solver(kissat, minisat)]\
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+|\
+| #[kani::solver(kissat, minisat)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 error: aborting due to previous error

tests/ui/solver-attribute/multiple-attrs/expected

@@ -1,6 +1,6 @@
 error: only one '#[kani::solver]' attribute is allowed per harness\
 test.rs:\
-  |\
-5 | #[kani::solver(kissat)]\
-  | ^^^^^^^^^^^^^^^^^^^^^^^
+|\
+| #[kani::solver(kissat)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^
 error: aborting due to previous error

tests/ui/solver-attribute/no-arg/expected

@@ -1,6 +1,6 @@
 error: the `#[kani::solver]` attribute expects a single argument. Got 0 arguments.\
 test.rs:\
-  |\
-5 | #[kani::solver]\
-  | ^^^^^^^^^^^^^^^
+|\
+| #[kani::solver]\
+| ^^^^^^^^^^^^^^^
 error: aborting due to previous error

tests/ui/solver-attribute/not-found/test.rs

@@ -4,5 +4,5 @@
 //! Checks that Kani errors out if specified solver binary is not found
 
 #[kani::proof]
-#[kani::solver(custom = "non_existing_solver")]
+#[kani::solver(bin = "non_existing_solver")]
 fn check() {}

tests/ui/solver-attribute/unknown/expected

@@ -1,6 +1,6 @@
 error: unknown solver `foo`\
 test.rs:\
-  |\
-5 | #[kani::solver(foo)]\
-  | ^^^^^^^^^^^^^^^^^^^^
+|\
+| #[kani::solver(foo)]\
+| ^^^^^^^^^^^^^^^^^^^^
 error: aborting due to previous error

tests/ui/solver-option/custom/expected renamed to tests/ui/solver-option/bin/expected

@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver custom=kissat
+// kani-flags: --solver bin=kissat
 
-//! Checks that `--solver` accepts `custom=<binary>`
+//! Checks that `--solver` accepts `bin=<binary>`
 
 #[kani::proof]
 fn check_solver_option() {