-Z uninit-checks automatically enables shadow memory

model-checking · Jul 8, 2024 · b388458 · b388458
1 parent 898dd0b
commit b388458
Show file tree

Hide file tree

Showing 19 changed files with 22 additions and 19 deletions.
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -140,7 +140,10 @@ impl KaniSession {
         }
 
         if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) {
-            flags.push("--ub-check=uninit".into())
+            // Automatically enable shadow memory, since the version of uninitialized memory checks
+            // without non-determinism depends on it.
+            flags.push("-Z ghost-state".into());
+            flags.push("--ub-check=uninit".into());
         }
 
         if self.args.ignore_locals_lifetime {

diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr::addr_of;
 

diff --git a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 #[repr(C)]

diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::alloc::{alloc, Layout};
 use std::slice::from_raw_parts;

diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 #![feature(core_intrinsics)]
 

diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 //! Checks that Kani supports memory initialization checks via intrinsics.
 
 #![feature(core_intrinsics)]

diff --git a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ops::Index;
 

diff --git a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 /// Checks that Kani catches an attempt to read uninitialized memory from a semi-initialized vector.
 #[kani::proof]

diff --git a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 /// Checks that Kani catches an attempt to read uninitialized memory from an uninitialized vector.
 #[kani::proof]

diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;

diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;

diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/kani/Uninit/access-padding-enum-single-field.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;

diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/kani/Uninit/access-padding-enum-single-variant.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr;
 use std::ptr::addr_of;

diff --git a/tests/kani/Uninit/access-padding-init.rs b/tests/kani/Uninit/access-padding-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr::addr_of;
 

diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::alloc::{alloc, Layout};
 

diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::alloc::{alloc_zeroed, Layout};
 use std::slice::from_raw_parts;

diff --git a/tests/kani/Uninit/atomic.rs b/tests/kani/Uninit/atomic.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::sync::atomic::{AtomicUsize, Ordering};
 

diff --git a/tests/kani/Uninit/struct-padding-and-arr-init.rs b/tests/kani/Uninit/struct-padding-and-arr-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 use std::ptr::addr_of_mut;
 

diff --git a/tests/kani/Uninit/vec-read-init.rs b/tests/kani/Uninit/vec-read-init.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ghost-state -Z uninit-checks
+// kani-flags: -Z uninit-checks
 
 #[kani::proof]
 fn vec_read_init() {