model-checking
diff --git a/‎.github/workflows/goto-transcoder.yml‎
Lines changed: 0 additions & 2 deletions b/‎.github/workflows/goto-transcoder.yml‎
Lines changed: 0 additions & 2 deletions
diff --git a/‎.github/workflows/kani-metrics.yml‎
Lines changed: 1 addition & 3 deletions b/‎.github/workflows/kani-metrics.yml‎
Lines changed: 1 addition & 3 deletions
diff --git a/‎.github/workflows/kani.yml‎
Lines changed: 1 addition & 12 deletions b/‎.github/workflows/kani.yml‎
Lines changed: 1 addition & 12 deletions
diff --git a/‎library/Cargo.lock‎
Lines changed: 9 additions & 10 deletions b/‎library/Cargo.lock‎
Lines changed: 9 additions & 10 deletions
diff --git a/‎library/Cargo.toml‎
Lines changed: 11 additions & 2 deletions b/‎library/Cargo.toml‎
Lines changed: 11 additions & 2 deletions
diff --git a/‎library/alloc/src/alloc.rs‎
Lines changed: 4 additions & 3 deletions b/‎library/alloc/src/alloc.rs‎
Lines changed: 4 additions & 3 deletions
diff --git a/‎library/alloc/src/collections/btree/set.rs‎
Lines changed: 1 addition & 3 deletions b/‎library/alloc/src/collections/btree/set.rs‎
Lines changed: 1 addition & 3 deletions
@@ -27,8 +27,6 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
-      - name: Apply stdarch patch
-        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Generate contracts programs
       - name: Generate contracts
 
@@ -25,9 +25,7 @@ jobs:
       uses: actions/checkout@v4
       with:
         submodules: true
-    - name: Apply stdarch patch
-      run: cd library/stdarch && patch -p1 < ../../stdarch.patch
-
+    
     # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
     - name: Set up Python
       uses: actions/setup-python@v4
 
@@ -51,9 +51,7 @@ jobs:
         with:
           path: head
           submodules: true
-      - name: Apply stdarch patch
-        run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
-
+      
       # Step 2: Install jq
       - name: Install jq
         if: matrix.os == 'ubuntu-latest'
@@ -90,8 +88,6 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
-      - name: Apply stdarch patch
-        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run Kani autoharness on the std library for selected functions.
       # Uses "--include-pattern" to make sure we do not try to run across all
@@ -102,8 +98,6 @@ jobs:
       # - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
       #   as whitespace is not supported, cf.
       #   https://github.com/model-checking/kani/issues/4046
-      # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
-      #   core_arch::x86:: functions that are known to verify successfully.
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
@@ -113,7 +107,6 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
-            --include-pattern core_arch::x86::__m128d::as_f64x2 \
             --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
@@ -295,8 +288,6 @@ jobs:
         with:
           path: head
           submodules: true
-      - name: Apply stdarch patch
-        run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run list on the std library
       - name: Run Kani List
@@ -329,8 +320,6 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
-      - name: Apply stdarch patch
-        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run autoharness analyzer on the std library
       - name: Run Autoharness Analyzer
 
@@ -1,3 +1,5 @@
+cargo-features = ["profile-rustflags"]
+
 [workspace]
 resolver = "1"
 members = [
@@ -44,9 +46,16 @@ object.debug = 0
 rustc-demangle.debug = 0
 rustc-demangle.opt-level = "s"
 
+# panic_abort must always be compiled with panic=abort, even when the rest of the
+# sysroot is panic=unwind.
+[profile.dev.package.panic_abort]
+rustflags = ["-Cpanic=abort"]
+
+[profile.release.package.panic_abort]
+rustflags = ["-Cpanic=abort"]
+
 [patch.crates-io]
-# See comments in `library/rustc-std-workspace-core/README.md` for what's going on
-# here
+# See comments in `library/rustc-std-workspace-core/README.md` for what's going on here
 rustc-std-workspace-core = { path = 'rustc-std-workspace-core' }
 rustc-std-workspace-alloc = { path = 'rustc-std-workspace-alloc' }
 rustc-std-workspace-std = { path = 'rustc-std-workspace-std' }
 
@@ -31,8 +31,9 @@ unsafe extern "Rust" {
     #[rustc_std_internal_symbol]
     fn __rust_alloc_zeroed(size: usize, align: usize) -> *mut u8;
 
+    #[rustc_nounwind]
     #[rustc_std_internal_symbol]
-    static __rust_no_alloc_shim_is_unstable: u8;
+    fn __rust_no_alloc_shim_is_unstable_v2();
 }
 
 /// The global memory allocator.
@@ -88,7 +89,7 @@ pub unsafe fn alloc(layout: Layout) -> *mut u8 {
     unsafe {
         // Make sure we don't accidentally allow omitting the allocator shim in
         // stable code until it is actually stabilized.
-        core::ptr::read_volatile(&__rust_no_alloc_shim_is_unstable);
+        __rust_no_alloc_shim_is_unstable_v2();
 
         __rust_alloc(layout.size(), layout.align())
     }
@@ -171,7 +172,7 @@ pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 {
     unsafe {
         // Make sure we don't accidentally allow omitting the allocator shim in
         // stable code until it is actually stabilized.
-        core::ptr::read_volatile(&__rust_no_alloc_shim_is_unstable);
+        __rust_no_alloc_shim_is_unstable_v2();
 
         __rust_alloc_zeroed(layout.size(), layout.align())
     }
 
@@ -1517,9 +1517,7 @@ impl<T: Ord, const N: usize> From<[T; N]> for BTreeSet<T> {
 
         // use stable sort to preserve the insertion order.
         arr.sort();
-        let iter = IntoIterator::into_iter(arr).map(|k| (k, SetValZST::default()));
-        let map = BTreeMap::bulk_build_from_sorted_iter(iter, Global);
-        BTreeSet { map }
+        BTreeSet::from_sorted_iter(IntoIterator::into_iter(arr), Global)
     }
 }
Original file line number	Diff line number	Diff line change
`@@ -1517,9 +1517,7 @@ impl<T: Ord, const N: usize> From<[T; N]> for BTreeSet<T> {`
`1517`	`1517`
`1518`	`1518`	`// use stable sort to preserve the insertion order.`
`1519`	`1519`	`arr.sort();`
`1520`		`- let iter = IntoIterator::into_iter(arr).map(\|k\| (k, SetValZST::default()));`
`1521`		`- let map = BTreeMap::bulk_build_from_sorted_iter(iter, Global);`
`1522`		`- BTreeSet { map }`
	`1520`	`+ BTreeSet::from_sorted_iter(IntoIterator::into_iter(arr), Global)`
`1523`	`1521`	`}`
`1524`	`1522`	`}`
`1525`	`1523`