Bump rustc.

cargo-creusot/Cargo.toml

@@ -7,17 +7,17 @@ publish = false
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-clap = { version = "4.2.5", features = ["derive", "env"] }
-serde_json = { version = "1.0" }
-toml = { version = "0.5.8" }
-env_logger = "0.10"
+clap = { version = "4.5", features = ["derive", "env"] }
+serde_json = "1.0"
+toml = "0.8"
+env_logger = "0.11"
 serde = { version = "1.0", features = ["derive"] }
 why3 = { path = "../why3", features = ["serialize"] }
 creusot-args = {path = "../creusot-args"}
 creusot-setup = {path = "../creusot-setup"}
 anyhow = "1.0"
-cargo_metadata = "0.18.1"
-include_dir = "0.7.3"
-tempdir = "0.3.7"
-glob = "0.3.1"
+cargo_metadata = "0.19"
+include_dir = "0.7"
+tempdir = "0.3"
+glob = "0.3"
 

cargo-creusot/src/helpers.rs

@@ -1,7 +1,7 @@
 use std::path::PathBuf;
 
 use anyhow::Error;
-use cargo_metadata;
+use cargo_metadata::{self, CrateType};
 use creusot_args::options::CommonOptions;
 pub type Result<T> = anyhow::Result<T>;
 
@@ -27,8 +27,8 @@ pub(crate) fn get_crate(m: &cargo_metadata::Metadata) -> Result<String> {
     let target = package.targets.first().ok_or(Error::msg("No target found"))?;
     let krate_name = target.name.replace("-", "_");
     let krate_type = target.crate_types.first().ok_or(Error::msg("No crate type found"))?;
-    let krate_type = if krate_type == "lib" { "rlib" } else { krate_type };
-    Ok(krate_name + "_" + krate_type)
+    let krate_type = if krate_type == &CrateType::Lib { &CrateType::RLib } else { krate_type };
+    Ok(krate_name + "_" + &krate_type.to_string())
 }
 
 fn get_crate_() -> Result<String> {

creusot-args/Cargo.toml

@@ -7,6 +7,6 @@ publish = false
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-clap = { version = "4.2.5", features = ["derive", "env"] }
-serde = { version = "1.0.195", features = ["derive"] }
+clap = { version = "4.5", features = ["derive", "env"] }
+serde = { version = "1.0", features = ["derive"] }
 

creusot-contracts-dummy/Cargo.toml

@@ -12,6 +12,6 @@ proc-macro = true
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-quote = "1.0.35"
-proc-macro2 = "1.0.29"
+quote = "1.0"
+proc-macro2 = "1.0"
 

creusot-contracts-proc/Cargo.toml

@@ -12,9 +12,9 @@ proc-macro = true
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-quote = "1.0.35"
-uuid = { version = "1.3", features = ["v4"] }
+quote = "1.0"
+uuid = { version = "1.12", features = ["v4"] }
 pearlite-syn = { version = "0.3", path = "../pearlite-syn", features = ["full"] }
-syn = { version = "2.0.15"}
-proc-macro2 = "1.0.29"
+syn = { version = "2.0"}
+proc-macro2 = "1.0"
 

creusot-contracts-proc/src/invariant.rs

@@ -99,7 +99,7 @@ fn filter_invariants(
     let mut invariants = Vec::new();
     parse_push_invariant(&mut invariants, tag, invariant)?;
 
-    let attrs = attrs.extract_if(|attr| {
+    let attrs = attrs.extract_if(0.., |attr| {
         attr.path().get_ident().map_or(false, |i| i == "invariant" || i == "variant")
     });
     for attr in attrs {

creusot-contracts/Cargo.toml

@@ -10,7 +10,7 @@ description = "Provides contracts and logic helpers for Creusot"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [target.'cfg(creusot)'.dependencies]
-num-rational = "0.3.2"
+num-rational = "0.4"
 creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "0.3.0" }
 
 [target.'cfg(not(creusot))'.dependencies]

creusot-contracts/src/lib.rs

@@ -36,7 +36,6 @@
     allocator_api,
     unboxed_closures,
     tuple_trait,
-    strict_provenance,
     panic_internals,
     libstd_sys_internals,
     rt,
@@ -359,7 +358,7 @@ pub mod macros {
     ///     #[ensures(result == x + 1)]
     ///     pub(super) fn foo(x: Int) -> Int {
     ///         // ...
-    /// # x + 1    
+    /// # x + 1
     ///     }
     /// }
     ///

creusot-dev-config/Cargo.toml

@@ -7,5 +7,5 @@ publish = false
 [dependencies]
 creusot-setup = { path = "../creusot-setup" }
 anyhow = "1.0"
-which = "6.0"
+which = "7.0"
 

creusot-metadata/Cargo.toml

@@ -7,7 +7,7 @@ publish = false
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-indexmap = "2.7.0"
+indexmap = "2.7"
 
 [package.metadata.rust-analyzer]
 # This crate uses #[feature(rustc_private)].

creusot-rustc/Cargo.toml

@@ -9,8 +9,8 @@ publish = false
 [dependencies]
 serde_json = { version = "1.0" }
 creusot = { path = "../creusot", version = "0.3" }
-toml = "0.5.8"
-env_logger = "0.10"
+toml = "0.8"
+env_logger = "0.11"
 serde = { version = "1.0", features = ["derive"] }
 creusot-args = { path = "../creusot-args" }
 

creusot-rustc/src/main.rs

@@ -14,7 +14,7 @@ extern crate log;
 use creusot::callbacks::*;
 use creusot_args::CREUSOT_RUSTC_ARGS;
 use options::CreusotArgs;
-use rustc_driver::RunCompiler;
+use rustc_driver::run_compiler;
 use rustc_session::{config::ErrorOutputType, EarlyDiagCtxt};
 use std::{env, panic, process::Command};
 
@@ -73,11 +73,11 @@ fn setup_plugin() {
                 Ok(opts) => opts,
                 Err(msg) => panic!("Error: {msg}"),
             };
-            RunCompiler::new(&args, &mut ToWhy::new(opts)).run().unwrap();
+            run_compiler(&args, &mut ToWhy::new(opts))
         }
         _ => {
             args.push("--cfg=creusot".to_string());
-            RunCompiler::new(&args, &mut DefaultCallbacks).run().unwrap()
+            run_compiler(&args, &mut DefaultCallbacks)
         }
     }
 }

creusot-setup/Cargo.toml

@@ -7,13 +7,13 @@ publish = false
 [dependencies]
 creusot-args = {path = "../creusot-args"}
 serde = { version = "1.0", features = ["derive"] }
-toml = { version = "0.5.8", features = ["preserve_order"] }
-directories = "5.0"
-which = "6.0"
+toml = { version = "0.8", features = ["preserve_order"] }
+directories = "6.0"
+which = "7.0"
 anyhow = "1.0"
 reqwest = { version = "0.12", features = ["blocking"] }
 zip = "2.2"
 hex = "0.4"
 sha2 = "0.10"
-indoc = "2.0.5"
+indoc = "2.0"
 

creusot/Cargo.toml

@@ -7,32 +7,32 @@ license = "LGPL-2.1-or-later"
 publish = false
 
 [dependencies]
-itertools = "0.10"
+itertools = "0.14"
 log = "0.4"
 serde = { version = "1.0", features = ["derive"] }
 # Necessary as this introduces a version of `GraphMap` with no `Ord` bound.
 # If https://github.com/petgraph/petgraph/issues/646 is solved, go back to upstream.
 petgraph = { version = "0.6", git = "https://github.com/xldenis/petgraph", rev = "04cecb7" }
-indexmap = { version = "2.7.0", features = ["serde"] }
-toml = "0.5.8"
+indexmap = { version = "2.7", features = ["serde"] }
+toml = "0.8"
 why3 = { path = "../why3", features = ["serialize"] }
 creusot-metadata = { path = "../creusot-metadata" }
-include_dir = "0.7.3"
-tempdir = "0.3.7"
-serde_json = { version = "1.0" }
-lazy_static = "1.4.0"
+include_dir = "0.7"
+tempdir = "0.3"
+serde_json = "1.0"
+lazy_static = "1.5"
 pathdiff = "0.2"
 
 [dev-dependencies]
-clap = { version = "4.2", features = ["derive", "env"] }
-regex = "1.10.5"
+clap = { version = "4.5", features = ["derive", "env"] }
+regex = "1.11"
 glob = "*"
-assert_cmd = "1.0"
-similar = "2.2"
-termcolor = "1.1"
-arraydeque = "0.4"
+assert_cmd = "2.0"
+similar = "2.7"
+termcolor = "1.4"
+arraydeque = "0.5"
 creusot-contracts = { path = "../creusot-contracts", features = ["typechecker"] }
-escargot = { version = "0.5" }
+escargot = "0.5"
 creusot-setup = { path = "../creusot-setup" }
 libc = "0.2"
 

creusot/src/analysis/borrows.rs

@@ -1,22 +1,18 @@
-use rustc_borrowck::{
-    borrow_set::BorrowSet,
-    consumers::{
-        calculate_borrows_out_of_scope_at_location, BorrowIndex, PlaceConflictBias, PlaceExt,
-        RegionInferenceContext,
-    },
+use rustc_borrowck::consumers::{
+    calculate_borrows_out_of_scope_at_location, BorrowIndex, BorrowSet, PlaceConflictBias,
+    PlaceExt, RegionInferenceContext,
 };
 use rustc_data_structures::fx::FxIndexMap;
-use std::fmt;
+use rustc_index::bit_set::MixedBitSet;
 // This Source Code Form is subject to the terms of the Mozilla Public
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at https://mozilla.org/MPL/2.0/.
 //
-use rustc_index::bit_set::BitSet;
 use rustc_middle::{
-    mir::{self, Body, CallReturnPlaces, Location, Place, TerminatorEdges},
+    mir::{self, Body, Location, Place, TerminatorEdges},
     ty::TyCtxt,
 };
-use rustc_mir_dataflow::{fmt::DebugWithContext, AnalysisDomain, GenKill, GenKillAnalysis};
+use rustc_mir_dataflow::{Analysis, GenKill};
 
 pub struct Borrows<'a, 'mir, 'tcx> {
     tcx: TyCtxt<'tcx>,
@@ -46,10 +42,6 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
         Borrows { tcx, body, borrow_set, borrows_out_of_scope_at_location }
     }
 
-    pub fn location(&self, idx: BorrowIndex) -> &Location {
-        &self.borrow_set[idx].reserve_location
-    }
-
     /// Add all borrows to the kill set, if those borrows are out of scope at `location`.
     /// That means they went out of a nonlexical scope
     fn kill_loans_out_of_scope_at_location(
@@ -79,7 +71,7 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
 
         let other_borrows_of_local = self
             .borrow_set
-            .local_map
+            .local_map()
             .get(&place.local)
             .into_iter()
             .flat_map(|bs| bs.iter())
@@ -103,7 +95,7 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
             rustc_borrowck::consumers::places_conflict(
                 self.tcx,
                 self.body,
-                self.borrow_set[i].borrowed_place,
+                self.borrow_set[i].borrowed_place(),
                 place,
                 PlaceConflictBias::NoOverlap,
             )
@@ -113,32 +105,24 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
     }
 }
 
-impl<'tcx> AnalysisDomain<'tcx> for Borrows<'_, '_, 'tcx> {
-    type Domain = BitSet<BorrowIndex>;
+impl<'tcx> Analysis<'tcx> for Borrows<'_, '_, 'tcx> {
+    type Domain = MixedBitSet<BorrowIndex>;
 
     const NAME: &'static str = "borrows";
 
     fn bottom_value(&self, _: &mir::Body<'tcx>) -> Self::Domain {
         // bottom = nothing is reserved or activated yet;
-        BitSet::new_empty(self.borrow_set.len())
+        MixedBitSet::new_empty(self.borrow_set.location_map().len())
     }
 
     fn initialize_start_block(&self, _: &mir::Body<'tcx>, _: &mut Self::Domain) {
         // no borrows of code region_scopes have been taken prior to
         // function execution, so this method has no effect.
     }
-}
-
-impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
-    type Idx = BorrowIndex;
 
-    fn domain_size(&self, _: &mir::Body<'tcx>) -> usize {
-        self.borrow_set.len()
-    }
-
-    fn statement_effect(
+    fn apply_primary_statement_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         stmt: &mir::Statement<'tcx>,
         location: Location,
     ) {
@@ -150,11 +134,11 @@ impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
                     if !place.ignore_borrow(
                         self.tcx,
                         self.body,
-                        &self.borrow_set.locals_state_at_exit,
+                        &self.borrow_set.locals_state_at_exit(),
                     ) {
                         let index = self
                             .borrow_set
-                            .location_map
+                            .location_map()
                             .get_index_of(&location)
                             .map(BorrowIndex::from)
                             .unwrap_or_else(|| {
@@ -185,11 +169,12 @@ impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
             | mir::StatementKind::Coverage(..)
             | mir::StatementKind::Intrinsic(..)
             | mir::StatementKind::ConstEvalCounter
-            | mir::StatementKind::Nop => {}
+            | mir::StatementKind::Nop
+            | mir::StatementKind::BackwardIncompatibleDropHint { .. } => {}
         }
     }
 
-    fn terminator_effect<'mir>(
+    fn apply_primary_terminator_effect<'mir>(
         &mut self,
         trans: &mut Self::Domain,
         terminator: &'mir mir::Terminator<'tcx>,
@@ -208,18 +193,4 @@ impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
         }
         terminator.edges()
     }
-
-    fn call_return_effect(
-        &mut self,
-        _trans: &mut Self::Domain,
-        _block: mir::BasicBlock,
-        _return_places: CallReturnPlaces<'_, 'tcx>,
-    ) {
-    }
-}
-
-impl DebugWithContext<Borrows<'_, '_, '_>> for BorrowIndex {
-    fn fmt_with(&self, ctxt: &Borrows<'_, '_, '_>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:?}", ctxt.location(*self))
-    }
 }