Update rustc pin

charon/rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2024-10-23"
+channel = "nightly-2024-11-23"
 components = [ "rustc-dev", "llvm-tools-preview" ]

charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs

@@ -967,6 +967,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             // Used in the interpreter to check that const code doesn't run for too long or even
             // indefinitely.
             StatementKind::ConstEvalCounter => None,
+            // Semantically equivalent to `Nop`, used only for rustc lints.
+            StatementKind::BackwardIncompatibleDropHint { .. } => None,
             StatementKind::Nop => None,
         };
 

charon/src/bin/charon-driver/translate/translate_predicates.rs

@@ -143,7 +143,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             ClauseKind::WellFormed(_) => {
                 raise_error!(self, span, "Well-formedness clauses are unsupported")
             }
-            kind @ ClauseKind::ConstEvaluatable(_) => {
+            kind => {
                 raise_error!(self, span, "Unsupported clause: {:?}", kind)
             }
         }

charon/src/bin/charon-driver/translate/translate_types.rs

@@ -21,9 +21,9 @@ fn check_region_name(s: String) -> Option<String> {
 pub fn translate_bound_region_kind_name(kind: &hax::BoundRegionKind) -> Option<String> {
     use hax::BoundRegionKind::*;
     let s = match kind {
-        BrAnon => None,
-        BrNamed(_, symbol) => Some(symbol.clone()),
-        BrEnv => Some("@env".to_owned()),
+        Anon => None,
+        Named(_, symbol) => Some(symbol.clone()),
+        ClosureEnv => Some("@env".to_owned()),
     };
     s.and_then(check_region_name)
 }

charon/tests/ui/external.out

@@ -171,6 +171,7 @@ pub fn test_crate::test_vec_push()
     return
 }
 
+#[lang_item("Cell")]
 pub opaque type core::cell::Cell<T>
 
 pub fn core::cell::{core::cell::Cell<T>}#10::get<'_0, T>(@1: &'_0 (core::cell::Cell<T>)) -> T

charon/tests/ui/issue-45-misc.out

@@ -173,7 +173,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60 : core::cmp::P
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::partial_cmp<'_0_0, '_0_1>
 }
 
-pub fn core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward_checked(@1: u8, @2: usize) -> core::option::Option<u8>[core::marker::Sized<u8>]
 
@@ -381,7 +381,7 @@ pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self)
 
 pub fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
 
-pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::Step::forward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 

charon/tests/ui/loops.out

@@ -767,7 +767,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76 : core::cmp:
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::partial_cmp<'_0_0, '_0_1>
 }
 
-pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked(@1: i32, @2: usize) -> core::option::Option<i32>[core::marker::Sized<i32>]
 
@@ -806,7 +806,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58 : core::
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<'_0_0, '_0_1>
 }
 
-pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_checked(@1: usize, @2: usize) -> core::option::Option<usize>[core::marker::Sized<usize>]
 
@@ -976,7 +976,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64 : core::cmp:
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::partial_cmp<'_0_0, '_0_1>
 }
 
-pub fn core::iter::range::{impl core::iter::range::Step for u32}#39::steps_between<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::{impl core::iter::range::Step for u32}#39::steps_between<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::{impl core::iter::range::Step for u32}#39::forward_checked(@1: u32, @2: usize) -> core::option::Option<u32>[core::marker::Sized<u32>]
 
@@ -1470,7 +1470,7 @@ where
     fn index_mut<'_0> = alloc::vec::{impl core::ops::index::IndexMut<I> for alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause2]}#14::index_mut<'_0_0, T, I, A>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3]
 }
 
-pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::Step::forward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 

charon/tests/ui/no_nested_borrows.out

@@ -277,11 +277,11 @@ pub fn test_crate::test_list1()
     return
 }
 
-pub fn alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#39::deref_mut<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box<T>[@TraitClause0])) -> &'_0 mut (T)
+pub fn alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#25::deref_mut<'_0, T, A>(@1: &'_0 mut (alloc::boxed::Box<T>[@TraitClause0])) -> &'_0 mut (T)
 where
     [@TraitClause0]: core::marker::Sized<A>,
 
-pub fn alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#38::deref<'_0, T, A>(@1: &'_0 (alloc::boxed::Box<T>[@TraitClause0])) -> &'_0 (T)
+pub fn alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#24::deref<'_0, T, A>(@1: &'_0 (alloc::boxed::Box<T>[@TraitClause0])) -> &'_0 (T)
 where
     [@TraitClause0]: core::marker::Sized<A>,
 
@@ -300,12 +300,12 @@ pub fn test_crate::test_box1()
     b@1 := @BoxNew<i32>[core::marker::Sized<i32>](const (0 : i32))
     @fake_read(b@1)
     @3 := &two-phase-mut b@1
-    x@2 := alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#39::deref_mut<'_, i32, alloc::alloc::Global>[core::marker::Sized<alloc::alloc::Global>](move (@3))
+    x@2 := alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#25::deref_mut<'_, i32, alloc::alloc::Global>[core::marker::Sized<alloc::alloc::Global>](move (@3))
     drop @3
     @fake_read(x@2)
     *(x@2) := const (1 : i32)
     @5 := &b@1
-    x@4 := alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#38::deref<'_, i32, alloc::alloc::Global>[core::marker::Sized<alloc::alloc::Global>](move (@5))
+    x@4 := alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#24::deref<'_, i32, alloc::alloc::Global>[core::marker::Sized<alloc::alloc::Global>](move (@5))
     drop @5
     @fake_read(x@4)
     @8 := copy (*(x@4))
@@ -624,20 +624,20 @@ pub trait core::ops::deref::DerefMut<Self>
 #[lang_item("deref_mut_method")]
 pub fn core::ops::deref::DerefMut::deref_mut<'_0, Self>(@1: &'_0 mut (Self)) -> &'_0 mut (Self::parent_clause0::Target)
 
-impl alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#38<T, A> : core::ops::deref::Deref<alloc::boxed::Box<T>[@TraitClause0]>
+impl alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#24<T, A> : core::ops::deref::Deref<alloc::boxed::Box<T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<A>,
 {
     type Target = T
-    fn deref<'_0> = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#38::deref<'_0_0, T, A>[@TraitClause0]
+    fn deref<'_0> = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#24::deref<'_0_0, T, A>[@TraitClause0]
 }
 
-impl alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#39<T, A> : core::ops::deref::DerefMut<alloc::boxed::Box<T>[@TraitClause0]>
+impl alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#25<T, A> : core::ops::deref::DerefMut<alloc::boxed::Box<T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<A>,
 {
-    parent_clause0 = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#38<T, A>[@TraitClause0]
-    fn deref_mut<'_0> = alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#39::deref_mut<'_0_0, T, A>[@TraitClause0]
+    parent_clause0 = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box<T>[@TraitClause0]}#24<T, A>[@TraitClause0]
+    fn deref_mut<'_0> = alloc::boxed::{impl core::ops::deref::DerefMut for alloc::boxed::Box<T>[@TraitClause0]}#25::deref_mut<'_0_0, T, A>[@TraitClause0]
 }
 
 #[lang_item("deref_method")]

charon/tests/ui/rvalues.rs

@@ -1,4 +1,3 @@
-#![feature(const_ub_checks)]
 #![feature(core_intrinsics)]
 #![feature(rustc_attrs)]
 #![allow(internal_features)]

charon/tests/ui/simple/gat-default.out

@@ -1,4 +1,4 @@
-thread 'rustc' panicked at /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/compiler/rustc_type_ir/src/binder.rs:697:9:
+thread 'rustc' panicked at /rustc/a47555110cf09b3ed59811d9b02235443e76a595/compiler/rustc_type_ir/src/binder.rs:735:9:
 type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()]
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Hax panicked when translating `test_crate::{impl#0}`.
@@ -22,7 +22,7 @@ error: Item `test_crate::Collection` caused errors; ignoring.
   | ^^^^^^^^^^^^^^^^
   |
 
-thread 'rustc' panicked at /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/compiler/rustc_type_ir/src/binder.rs:697:9:
+thread 'rustc' panicked at /rustc/a47555110cf09b3ed59811d9b02235443e76a595/compiler/rustc_type_ir/src/binder.rs:735:9:
 type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()]
 error: Hax panicked when translating `test_crate::{impl#0}`.
  --> tests/ui/simple/gat-default.rs:9:1

charon/tests/ui/ullbc-control-flow.out

@@ -110,7 +110,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76 : core::cmp:
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::partial_cmp<'_0_0, '_0_1>
 }
 
-pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked(@1: i32, @2: usize) -> core::option::Option<i32>[core::marker::Sized<i32>]
 
@@ -149,7 +149,7 @@ impl core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58 : core::
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<'_0_0, '_0_1>
 }
 
-pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_checked(@1: usize, @2: usize) -> core::option::Option<usize>[core::marker::Sized<usize>]
 
@@ -375,7 +375,7 @@ where
 #[lang_item("next")]
 pub fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option<Self::Item>[Self::parent_clause0]
 
-pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::option::Option<usize>[core::marker::Sized<usize>]
+pub fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
 
 pub fn core::iter::range::Step::forward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]