diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 72de44e36014..573ad21ab31a 100644 --- a/kani-driver/src/args/mod.rs +++ b/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, @@ -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 { diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index beddd7cc580e..2dc2bd2a4957 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -25,7 +25,7 @@ //! simple division function `my_div`: //! //! ``` -//! fn my_div(dividend: u32, divisor: u32) -> u32 { +//! fn my_div(dividend: usize, divisor: usize) -> usize { //! dividend / divisor //! } //! ``` @@ -35,8 +35,12 @@ //! allows us to declare constraints on what constitutes valid inputs to our //! function. In this case we would want to disallow a divisor that is `0`. //! -//! ```ignore +//! ``` +//! # use kani::requires; //! #[requires(divisor != 0)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } //! ``` //! //! This is called a precondition, because it is enforced before (pre-) the @@ -51,7 +55,11 @@ //! approximation of the result of division for instance could be this: //! //! ``` -//! #[ensures(|result : &u32| *result <= dividend)] +//! # use kani::ensures; +//! #[ensures(|result : &usize| *result <= dividend)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } //! ``` //! //! This is called a postcondition and it also has access to the arguments and @@ -66,9 +74,11 @@ //! order does not matter. In our example putting them together looks like this: //! //! ``` -//! #[kani::requires(divisor != 0)] -//! #[kani::ensures(|result : &u32| *result <= dividend)] -//! fn my_div(dividend: u32, divisor: u32) -> u32 { +//! use kani::{requires, ensures}; +//! +//! #[requires(divisor != 0)] +//! #[ensures(|result : &usize| *result <= dividend)] +//! fn my_div(dividend: usize, divisor: usize) -> usize { //! dividend / divisor //! } //! ``` @@ -84,9 +94,18 @@ //! function we want to check. //! //! ``` +//! # use kani::{requires, ensures}; +//! # +//! # #[requires(divisor != 0)] +//! # #[ensures(|result : &usize| *result <= dividend)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } +//! # //! #[kani::proof_for_contract(my_div)] //! fn my_div_harness() { -//! my_div(kani::any(), kani::any()) } +//! my_div(kani::any(), kani::any()); +//! } //! ``` //! //! The harness is checked like any other by running `cargo kani` and can be @@ -104,10 +123,18 @@ //! the contract will be used automatically. //! //! ``` +//! # use kani::{requires, ensures}; +//! # +//! # #[requires(divisor != 0)] +//! # #[ensures(|result : &usize| *result <= dividend)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } +//! # //! #[kani::proof] //! #[kani::stub_verified(my_div)] //! fn use_div() { -//! let v = vec![...]; +//! let v = kani::vec::any_vec::(); //! let some_idx = my_div(v.len() - 1, 3); //! v[some_idx]; //! } diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs index 068cdedc277e..b1bac031b677 100644 --- a/library/kani/src/invariant.rs +++ b/library/kani/src/invariant.rs @@ -39,6 +39,14 @@ /// ``` /// You can specify its safety invariant as: /// ```rust +/// # #[derive(kani::Arbitrary)] +/// # pub struct MyDate { +/// # day: u8, +/// # month: u8, +/// # year: i64, +/// # } +/// # fn days_in_month(_: i64, _: u8) -> u8 { 31 } +/// /// impl kani::Invariant for MyDate { /// fn is_safe(&self) -> bool { /// self.month > 0 @@ -49,12 +57,33 @@ /// } /// ``` /// And use it to check that your APIs are safe: -/// ```rust +/// ```no_run +/// # use kani::Invariant; +/// # +/// # #[derive(kani::Arbitrary)] +/// # pub struct MyDate { +/// # day: u8, +/// # month: u8, +/// # year: i64, +/// # } +/// # +/// # fn days_in_month(_: i64, _: u8) -> u8 { todo!() } +/// # fn increase_date(_: &mut MyDate, _: u8) { todo!() } +/// # +/// # impl Invariant for MyDate { +/// # fn is_safe(&self) -> bool { +/// # self.month > 0 +/// # && self.month <= 12 +/// # && self.day > 0 +/// # && self.day <= days_in_month(self.year, self.month) +/// # } +/// # } +/// # /// #[kani::proof] /// fn check_increase_date() { /// let mut date: MyDate = kani::any(); /// // Increase date by one day -/// increase_date(date, 1); +/// increase_date(&mut date, 1); /// assert!(date.is_safe()); /// } /// ``` diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 053af760067b..ce1eeb992121 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -19,6 +19,8 @@ #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] +// Need to add this since we are deprecating `kani::check`. Remove this when we remove that API. +#![allow(deprecated)] // Allow us to use `kani::` to access crate features. extern crate self as kani; diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index a7ea57c6fd40..48ce8f0f9211 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -10,7 +10,7 @@ //! //! # Example //! -//! ``` +//! ```no_run //! use kani::shadow::ShadowMem; //! use std::alloc::{alloc, Layout}; //! diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs index 1b13de29d589..c419a881fa55 100644 --- a/library/kani/src/slice.rs +++ b/library/kani/src/slice.rs @@ -9,7 +9,8 @@ use crate::{any, assume}; /// /// # Example: /// -/// ```rust +/// ```no_run +/// # fn foo(_: &[i32]) {} /// let arr = [1, 2, 3]; /// let slice = kani::slice::any_slice_of_array(&arr); /// foo(slice); // where foo is a function that takes a slice and verifies a property about it diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 5df8f2228c62..839313f084c2 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -42,6 +42,7 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(core); kani_core::generate_arbitrary!(core); + kani_core::check_intrinsic!(); pub mod mem { kani_core::kani_mem!(core); @@ -58,6 +59,10 @@ macro_rules! kani_lib { kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); + kani_core::check_intrinsic! { + msg="This API will be made private in future releases.", vis=pub + } + pub mod mem { kani_core::kani_mem!(std); } @@ -85,7 +90,7 @@ macro_rules! kani_intrinsics { /// /// The code snippet below should never panic. /// - /// ```rust + /// ```no_run /// let i : i32 = kani::any(); /// kani::assume(i > 10); /// if i < 0 { @@ -95,7 +100,7 @@ macro_rules! kani_intrinsics { /// /// The following code may panic though: /// - /// ```rust + /// ```no_run /// let i : i32 = kani::any(); /// assert!(i < 0, "This may panic and verification should fail."); /// kani::assume(i > 10); @@ -118,7 +123,7 @@ macro_rules! kani_intrinsics { /// /// # Example: /// - /// ```rust + /// ```no_run /// let x: bool = kani::any(); /// let y = !x; /// kani::assert(x || y, "ORing a boolean variable with its negation must be true") @@ -138,35 +143,15 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } - /// Creates an assertion of the specified condition and message, but does not assume it afterwards. - /// - /// # Example: - /// - /// ```rust - /// let x: bool = kani::any(); - /// let y = !x; - /// kani::check(x || y, "ORing a boolean variable with its negation must be true") - /// ``` - #[cfg(not(feature = "concrete_playback"))] - #[inline(never)] - #[rustc_diagnostic_item = "KaniCheck"] - pub const fn check(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; - } - - #[cfg(feature = "concrete_playback")] - #[inline(never)] - #[rustc_diagnostic_item = "KaniCheck"] - pub const fn check(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); - } - /// Creates a cover property with the specified condition and message. /// /// # Example: /// - /// ```rust + /// ```no_run + /// # use crate::kani; + /// # + /// # let array: [u8; 10] = kani::any(); + /// # let slice = kani::slice::any_slice_of_array(&array); /// kani::cover(slice.len() == 0, "The slice may have a length of 0"); /// ``` /// @@ -193,7 +178,11 @@ macro_rules! kani_intrinsics { /// In the snippet below, we are verifying the behavior of the function `fn_under_verification` /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. /// - /// ```rust + /// ```no_run + /// # use std::num::NonZeroU8; + /// # use crate::kani; + /// # + /// # fn fn_under_verification(_: NonZeroU8) {} /// let inputA = kani::any::(); /// fn_under_verification(inputA); /// ``` @@ -231,7 +220,11 @@ macro_rules! kani_intrinsics { /// In the snippet below, we are verifying the behavior of the function `fn_under_verification` /// under all possible `u8` input values between 0 and 12. /// - /// ```rust + /// ```no_run + /// # use std::num::NonZeroU8; + /// # use crate::kani; + /// # + /// # fn fn_under_verification(_: u8) {} /// let inputA: u8 = kani::any_where(|x| *x < 12); /// fn_under_verification(inputA); /// ``` @@ -460,3 +453,48 @@ macro_rules! kani_intrinsics { } }; } + +#[macro_export] +macro_rules! check_intrinsic { + ($(msg=$msg:literal, vis=$vis:vis)?) => { + /// Creates a non-fatal property with the specified condition and message. + /// + /// This check will not impact the program control flow even when it fails. + /// + /// # Example: + /// + /// ```no_run + /// let x: bool = kani::any(); + /// let y = !x; + /// kani::check(x || y, "ORing a boolean variable with its negation must be true"); + /// kani::check(x == y, "A boolean variable is always different than its negation"); + /// kani::cover!(true, "This should still be reachable"); + /// ``` + /// + /// # Deprecated + /// + /// This function was meant to be internal only, and it was added to Kani's public interface + /// by mistake. Thus, it will be made private in future releases. + /// Instead, we recommend users to either use `assert` or `cover` to create properties they + /// would like to verify. + /// + /// See for more details. + #[cfg(not(feature = "concrete_playback"))] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + // TODO: Remove the `#![allow(deprecated)]` inside kani's crate once this is made private. + $(#[deprecated(since="0.55.0", note=$msg)])? + $($vis)? const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; + } + + #[cfg(feature = "concrete_playback")] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + $(#[deprecated(since="0.55.0", note=$msg)])? + $($vis)? const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); + } + }; +} diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c0fba0261fa7..7ef640dbfdc9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-10-01" +channel = "nightly-2024-10-03" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 7acafbe8a1ed..728129d784b6 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -41,8 +41,8 @@ cargo test -p cprover_bindings cargo test -p kani-compiler cargo test -p kani-driver cargo test -p kani_metadata -# skip doc tests and enable assertions to fail -cargo test -p kani --lib --features concrete_playback +# Use concrete playback to enable assertions failure +cargo test -p kani --features concrete_playback # Test the actual macros, skipping doc tests and enabling extra traits for "syn" # so we can debug print AST RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib diff --git a/tests/cargo-kani/asm/global/Cargo.toml b/tests/cargo-kani/asm/global/Cargo.toml index 21ff904a2f99..79ffab9377c1 100644 --- a/tests/cargo-kani/asm/global/Cargo.toml +++ b/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 } diff --git a/tests/cargo-kani/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml index 39d5016a407b..f00d4c687864 100644 --- a/tests/cargo-kani/mir-linker/Cargo.toml +++ b/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 } diff --git a/tests/cargo-ui/ws-integ-tests/Cargo.toml b/tests/cargo-ui/ws-integ-tests/Cargo.toml index b09d4c9a5f19..93c4baebe120 100644 --- a/tests/cargo-ui/ws-integ-tests/Cargo.toml +++ b/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 diff --git a/tests/kani/UnsizedCoercion/basic_coercion.rs b/tests/kani/UnsizedCoercion/basic_coercion.rs index a60a76aec3be..ee8c80e87011 100644 --- a/tests/kani/UnsizedCoercion/basic_coercion.rs +++ b/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. diff --git a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs index efc84b61ea1e..19d8f39fed7e 100644 --- a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs +++ b/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. diff --git a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs index a2b5bfae3129..633dfbdaa995 100644 --- a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs +++ b/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. diff --git a/tests/kani/UnsizedCoercion/box_coercion.rs b/tests/kani/UnsizedCoercion/box_coercion.rs index e022bdef06e1..106f586f8eed 100644 --- a/tests/kani/UnsizedCoercion/box_coercion.rs +++ b/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. diff --git a/tests/kani/UnsizedCoercion/box_inner_coercion.rs b/tests/kani/UnsizedCoercion/box_inner_coercion.rs index 35f10373d5ef..4e8a8b56624c 100644 --- a/tests/kani/UnsizedCoercion/box_inner_coercion.rs +++ b/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. diff --git a/tests/kani/UnsizedCoercion/box_outer_coercion.rs b/tests/kani/UnsizedCoercion/box_outer_coercion.rs index 586f54003cdf..2d91360cd576 100644 --- a/tests/kani/UnsizedCoercion/box_outer_coercion.rs +++ b/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; diff --git a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs index 7f7d68ef6e84..6d75204223c1 100644 --- a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs +++ b/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)] diff --git a/tests/kani/UnsizedCoercion/double_coercion.rs b/tests/kani/UnsizedCoercion/double_coercion.rs index 26cfb585821e..76158c811c00 100644 --- a/tests/kani/UnsizedCoercion/double_coercion.rs +++ b/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. diff --git a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs index 2543498cca80..7a608d7d1d57 100644 --- a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs +++ b/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; diff --git a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs index 32875f8b8e22..b7750db487e2 100644 --- a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs +++ b/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. diff --git a/tests/perf/string/src/any_str.rs b/tests/perf/string/src/any_str.rs index 3b58d56750a7..6b3f9cffbc37 100644 --- a/tests/perf/string/src/any_str.rs +++ b/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)] diff --git a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs index a0c1bef7d003..596bedaa7825 100644 --- a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs +++ b/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 diff --git a/tests/ui/check_deprecated/deprecated_warning.expected b/tests/ui/check_deprecated/deprecated_warning.expected new file mode 100644 index 000000000000..3a0760035f8b --- /dev/null +++ b/tests/ui/check_deprecated/deprecated_warning.expected @@ -0,0 +1 @@ +warning: use of deprecated function `kani::check`: This API will be made private in future releases. diff --git a/tests/ui/check_deprecated/deprecated_warning.rs b/tests/ui/check_deprecated/deprecated_warning.rs new file mode 100644 index 000000000000..f3d791256081 --- /dev/null +++ b/tests/ui/check_deprecated/deprecated_warning.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: --only-codegen + +/// Ensure that Kani prints a deprecation warning if users invoke `kani::check`. +#[kani::proof] +fn internal_api() { + kani::check(kani::any(), "oops"); +} diff --git a/tests/ui/mir-linker/generic-harness/incorrect.rs b/tests/ui/mir-linker/generic-harness/incorrect.rs index e68eba6ec834..e52b06801517 100644 --- a/tests/ui/mir-linker/generic-harness/incorrect.rs +++ b/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]