Skip to content

Commit 3a06fe9

Browse files
author
Carolyn Zech
committed
update to 6/6
1 parent 241f2ed commit 3a06fe9

File tree

6 files changed

+8
-8
lines changed

6 files changed

+8
-8
lines changed

cprover_bindings/src/irep/irep_id.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -887,7 +887,7 @@ impl ToString for IrepId {
887887
}
888888

889889
impl IrepId {
890-
pub fn to_string_cow(&self) -> Cow<str> {
890+
pub fn to_string_cow(&self) -> Cow<'_, str> {
891891
match self.to_owned_string() {
892892
Some(owned) => Cow::Owned(owned),
893893
None => Cow::Borrowed(self.to_static_string()),

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -519,7 +519,7 @@ impl GotocCtx<'_> {
519519
.index_by_increasing_offset()
520520
.map(|idx| {
521521
let field_ty = layout.field(self, idx).ty;
522-
if idx == *discriminant_field {
522+
if idx == (*discriminant_field).as_usize() {
523523
Expr::int_constant(0, self.codegen_ty(field_ty))
524524
} else {
525525
self.codegen_operand_stable(&operands[idx])

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -914,7 +914,7 @@ impl<'tcx> GotocCtx<'tcx> {
914914
pretty_name,
915915
type_and_layout,
916916
"DirectFields".into(),
917-
Some(*discriminant_field),
917+
Some((*discriminant_field).as_usize()),
918918
),
919919
};
920920
let mut fields = vec![direct_fields];
@@ -1277,7 +1277,7 @@ impl<'tcx> GotocCtx<'tcx> {
12771277
// Contrary to coroutines, currently enums have only one field (the discriminant), the rest are in the variants:
12781278
assert!(layout.fields.count() <= 1);
12791279
// Contrary to coroutines, the discriminant is the first (and only) field for enums:
1280-
assert_eq!(*tag_field, 0);
1280+
assert_eq!((*tag_field).as_usize(), 0);
12811281
match tag_encoding {
12821282
TagEncoding::Direct => {
12831283
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| {

kani-compiler/src/kani_middle/provide.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,15 +28,15 @@ fn should_override(args: &Arguments) -> bool {
2828

2929
/// Returns the optimized code for the external function associated with `def_id` by
3030
/// running rustc's optimization passes followed by Kani-specific passes.
31-
fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body {
31+
fn run_mir_passes_extern(tcx: TyCtxt<'_>, def_id: DefId) -> &Body<'_> {
3232
tracing::debug!(?def_id, "run_mir_passes_extern");
3333
let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.extern_queries.optimized_mir)(tcx, def_id);
3434
run_kani_mir_passes(tcx, def_id, body)
3535
}
3636

3737
/// Returns the optimized code for the local function associated with `def_id` by
3838
/// running rustc's optimization passes followed by Kani-specific passes.
39-
fn run_mir_passes(tcx: TyCtxt, def_id: LocalDefId) -> &Body {
39+
fn run_mir_passes(tcx: TyCtxt<'_>, def_id: LocalDefId) -> &Body<'_> {
4040
tracing::debug!(?def_id, "run_mir_passes");
4141
let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir)(tcx, def_id);
4242
run_kani_mir_passes(tcx, def_id.to_def_id(), body)

library/kani_macros/src/sysroot/contracts/helpers.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use syn::spanned::Spanned;
1010
use syn::{Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt, parse_quote};
1111

1212
/// If an explicit return type was provided it is returned, otherwise `()`.
13-
pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<syn::Type> {
13+
pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<'_, syn::Type> {
1414
match return_type {
1515
syn::ReturnType::Default => Cow::Owned(syn::Type::Tuple(syn::TypeTuple {
1616
paren_token: syn::token::Paren::default(),

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-06-05"
5+
channel = "nightly-2025-06-06"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)