From c236c2077a73df4580f9fb4068a20ce95f99c6e1 Mon Sep 17 00:00:00 2001 From: Jacob Salzberg Date: Tue, 27 Aug 2024 13:59:42 -0400 Subject: [PATCH] Add copyright info --- tests/expected/aliasing/boxed.expected.fixme | 2 -- tests/expected/aliasing/control_flow.rs | 2 ++ tests/expected/aliasing/duplicate_write.rs | 2 ++ .../aliasing/duplicate_write_compressed.rs | 2 ++ .../aliasing/write_read_write.expected.fixme | 2 -- tests/expected/aliasing/write_read_write.rs.fixme | 14 -------------- 6 files changed, 6 insertions(+), 18 deletions(-) delete mode 100644 tests/expected/aliasing/boxed.expected.fixme delete mode 100644 tests/expected/aliasing/write_read_write.expected.fixme delete mode 100644 tests/expected/aliasing/write_read_write.rs.fixme diff --git a/tests/expected/aliasing/boxed.expected.fixme b/tests/expected/aliasing/boxed.expected.fixme deleted file mode 100644 index 40b69fbc424a..000000000000 --- a/tests/expected/aliasing/boxed.expected.fixme +++ /dev/null @@ -1,2 +0,0 @@ -FAILURE\ -assertion failed: Stack violated diff --git a/tests/expected/aliasing/control_flow.rs b/tests/expected/aliasing/control_flow.rs index 4a2fe04ff555..3b18b0f27cda 100644 --- a/tests/expected/aliasing/control_flow.rs +++ b/tests/expected/aliasing/control_flow.rs @@ -1,3 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zghost-state -Zaliasing #[allow(unused)] diff --git a/tests/expected/aliasing/duplicate_write.rs b/tests/expected/aliasing/duplicate_write.rs index 62ecec832f21..bf3a6d11b307 100644 --- a/tests/expected/aliasing/duplicate_write.rs +++ b/tests/expected/aliasing/duplicate_write.rs @@ -1,3 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zghost-state -Zaliasing #[kani::proof] diff --git a/tests/expected/aliasing/duplicate_write_compressed.rs b/tests/expected/aliasing/duplicate_write_compressed.rs index 1703b4799ee5..466d9f219ade 100644 --- a/tests/expected/aliasing/duplicate_write_compressed.rs +++ b/tests/expected/aliasing/duplicate_write_compressed.rs @@ -1,3 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zghost-state -Zaliasing #[kani::proof] diff --git a/tests/expected/aliasing/write_read_write.expected.fixme b/tests/expected/aliasing/write_read_write.expected.fixme deleted file mode 100644 index 40b69fbc424a..000000000000 --- a/tests/expected/aliasing/write_read_write.expected.fixme +++ /dev/null @@ -1,2 +0,0 @@ -FAILURE\ -assertion failed: Stack violated diff --git a/tests/expected/aliasing/write_read_write.rs.fixme b/tests/expected/aliasing/write_read_write.rs.fixme deleted file mode 100644 index dea1ab64c755..000000000000 --- a/tests/expected/aliasing/write_read_write.rs.fixme +++ /dev/null @@ -1,14 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zaliasing - -#[kani::proof] -fn main() { - let mut x = 10; - let ref_x = &mut x; - let raw_1 = ref_x as *mut i32; - let raw_2 = ref_x as *const i32; - let _write = unsafe { *raw_1 = 100 }; - let _read = unsafe { *raw_2 }; - let _write = unsafe { *raw_1 = 110 }; -}