Merge branch 'main' into dependabot/submodules/tests/perf/s2n-quic-cb…

…41b35

deny.toml

@@ -1,6 +1,12 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+[graph]
+# derivative is marked as unmaintained by RUSTSEC but still used in
+# Charon. We exclude it from the deny check until derivative is replaced
+# from Charon (https://github.com/AeneasVerif/charon/pull/459).
+exclude = ["derivative"]
+
 # This section is considered when running `cargo deny check advisories`
 # More documentation for the advisories section can be found here:
 # https://embarkstudios.github.io/cargo-deny/checks/advisories/cfg.html

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-11-03"
+channel = "nightly-2024-11-08"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/function-contract/const_fn_with_effect.rs

@@ -6,7 +6,6 @@
 //! Check that Kani contract can be applied to a constant function.
 //! <https://github.com/model-checking/kani/issues/3258>
 
-#![feature(effects)]
 #![allow(incomplete_features)]
 
 #[kani::requires(kani::mem::can_dereference(arg))]