Remove obsolete linker options (#3559)

These were made obsolete a while back.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

kani-driver/src/args/mod.rs

@@ -40,6 +40,7 @@ where
  .unwrap()
 }
 
+#[allow(dead_code)]
 pub fn print_obsolete(verbosity: &CommonArgs, option: &str) {
  if !verbosity.quiet {
  warning(&format!(
@@ -189,14 +190,6 @@ pub struct VerificationArgs {
  #[arg(long, hide_short_help = true)]
  pub only_codegen: bool,
 
- /// Deprecated flag. This is a no-op since we no longer support the legacy linker and
- /// it will be removed in a future Kani release.
- #[arg(long, hide = true, conflicts_with("mir_linker"))]
- pub legacy_linker: bool,
- /// Deprecated flag. This is a no-op since we no longer support any other linker.
- #[arg(long, hide = true)]
- pub mir_linker: bool,
-
  /// Specify the value used for loop unwinding in CBMC
  #[arg(long)]
  pub default_unwind: Option<u32>,
@@ -524,14 +517,6 @@ impl ValidateArgs for VerificationArgs {
  }
  }
 
- if self.mir_linker {
- print_obsolete(&self.common_args, "--mir-linker");
- }
-
- if self.legacy_linker {
- print_obsolete(&self.common_args, "--legacy-linker");
- }
-
  // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
  // We should consider improving the error messages slightly in a later pull request.
  if natives_unwind && extra_unwind {

tests/cargo-kani/asm/global/Cargo.toml

@@ -13,4 +13,4 @@ crate_with_global_asm = { path = "crate_with_global_asm" }
 
 [package.metadata.kani]
 # Issue with MIR Linker on static constant.
-flags = { enable-unstable = true, ignore-global-asm = true, mir-linker = true }
+flags = { enable-unstable = true, ignore-global-asm = true }

tests/cargo-kani/mir-linker/Cargo.toml

@@ -8,6 +8,3 @@ description = "Ensures that the mir-linker works accross crates"
 
 [dependencies]
 semver = "1.0"
-
-[package.metadata.kani]
-flags = { mir-linker=true, enable-unstable=true }

tests/cargo-ui/ws-integ-tests/Cargo.toml

@@ -15,5 +15,3 @@ members = [
 [workspace.metadata.kani.flags]
 workspace = true
 tests = true
-enable-unstable=true
-mir-linker=true

tests/kani/UnsizedCoercion/basic_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/kani/UnsizedCoercion/basic_inner_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/kani/UnsizedCoercion/basic_outer_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/kani/UnsizedCoercion/box_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using boxes.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/kani/UnsizedCoercion/box_inner_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using boxes.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/kani/UnsizedCoercion/box_outer_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using boxes.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 mod defs;

tests/kani/UnsizedCoercion/custom_outer_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using a custom CoerceUnsized implementation.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 #![feature(coerce_unsized)]

tests/kani/UnsizedCoercion/double_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using box of box.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/kani/UnsizedCoercion/rc_outer_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using reference counter.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 mod defs;

tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 

tests/perf/string/src/any_str.rs

@@ -1,10 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//
-// kani-flags: --enable-unstable --mir-linker
-//
-//! This test is to check MIR linker state of the art.
-//! I.e.: Currently, this should fail with missing function definition.
 
 #[kani::proof]
 #[kani::unwind(4)]

tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs

@@ -1,7 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --enable-unstable --mir-linker
 //! Make sure we can handle explicit copy_nonoverlapping on empty string
 //! This used to trigger an issue: https://github.com/model-checking/kani/issues/241
 

tests/ui/mir-linker/generic-harness/incorrect.rs

@@ -1,8 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --mir-linker
-//
 //! Checks that we correctly fail if the harness is a generic function.
 
 #[kani::proof]