Skip to content

Commit

Permalink
Remove --mir-linker from tests
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws committed Oct 1, 2024
1 parent fdfb51f commit 3853481
Show file tree
Hide file tree
Showing 16 changed files with 0 additions and 63 deletions.
13 changes: 0 additions & 13 deletions tests/cargo-kani/mir-linker/Cargo.toml

This file was deleted.

3 changes: 0 additions & 3 deletions tests/cargo-kani/mir-linker/expected

This file was deleted.

29 changes: 0 additions & 29 deletions tests/cargo-kani/mir-linker/src/lib.rs

This file was deleted.

1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/basic_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/basic_inner_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/basic_outer_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/box_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/box_inner_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/box_outer_coercion.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/custom_outer_coercion.rs
Original file line number Diff line number Diff line change
@@ -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)]
Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/double_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/rc_outer_coercion.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand Down
1 change: 0 additions & 1 deletion tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
5 changes: 0 additions & 5 deletions tests/perf/string/src/any_str.rs
Original file line number Diff line number Diff line change
@@ -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)]
Expand Down
1 change: 0 additions & 1 deletion tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs
Original file line number Diff line number Diff line change
@@ -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

Expand Down
2 changes: 0 additions & 2 deletions tests/ui/mir-linker/generic-harness/incorrect.rs
Original file line number Diff line number Diff line change
@@ -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]
Expand Down

0 comments on commit 3853481

Please sign in to comment.