Skip to content

Commit 2d23f1a

Browse files
authored
Upgrade to 2024-01-08 rust toolchain (#2969)
Relevant PRs: - rust-lang/rust#119601 - rust-lang/rust#119146 - rust-lang/rust#119174 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent b504ebf commit 2d23f1a

File tree

13 files changed

+75
-72
lines changed

13 files changed

+75
-72
lines changed

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -649,7 +649,7 @@ impl<'tcx> GotocCtx<'tcx> {
649649
pretty_ty(actual)
650650
),
651651
);
652-
self.tcx.sess.abort_if_errors();
652+
self.tcx.dcx().abort_if_errors();
653653
unreachable!("Rustc should have aborted already")
654654
}
655655

@@ -1303,7 +1303,7 @@ impl<'tcx> GotocCtx<'tcx> {
13031303
u64::MIN
13041304
})
13051305
};
1306-
self.tcx.sess.abort_if_errors();
1306+
self.tcx.dcx().abort_if_errors();
13071307
n
13081308
}
13091309

@@ -1432,7 +1432,7 @@ impl<'tcx> GotocCtx<'tcx> {
14321432
);
14331433
utils::span_err(self.tcx, span, err_msg);
14341434
}
1435-
self.tcx.sess.abort_if_errors();
1435+
self.tcx.dcx().abort_if_errors();
14361436

14371437
self.codegen_expr_to_place_stable(p, vec.index_array(index))
14381438
}
@@ -1472,7 +1472,7 @@ impl<'tcx> GotocCtx<'tcx> {
14721472
);
14731473
utils::span_err(self.tcx, span, err_msg);
14741474
}
1475-
self.tcx.sess.abort_if_errors();
1475+
self.tcx.dcx().abort_if_errors();
14761476

14771477
// Type checker should have ensured it's a vector type
14781478
let elem_ty = cbmc_ret_ty.base_type().unwrap().clone();
@@ -1550,7 +1550,7 @@ impl<'tcx> GotocCtx<'tcx> {
15501550
);
15511551
utils::span_err(self.tcx, span, err_msg);
15521552
}
1553-
self.tcx.sess.abort_if_errors();
1553+
self.tcx.dcx().abort_if_errors();
15541554

15551555
// Create the vector comparison expression
15561556
let e = f(arg1, arg2, ret_typ);
@@ -1773,7 +1773,7 @@ impl<'tcx> GotocCtx<'tcx> {
17731773
cond.ternary(t, e)
17741774
})
17751775
.collect();
1776-
self.tcx.sess.abort_if_errors();
1776+
self.tcx.dcx().abort_if_errors();
17771777
let cbmc_ret_ty = self.codegen_ty_stable(rust_ret_type);
17781778
self.codegen_expr_to_place_stable(p, Expr::vector_expr(cbmc_ret_ty, elems))
17791779
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
411411
}
412412
sig
413413
}
414-
ty::Coroutine(did, args, _) => self.coroutine_sig(did, fntyp, args),
414+
ty::Coroutine(did, args) => self.coroutine_sig(did, fntyp, args),
415415
_ => unreachable!("Can't get function signature of type: {:?}", fntyp),
416416
})
417417
}

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -417,10 +417,10 @@ fn check_target(session: &Session) {
417417
it is {}",
418418
&session.target.llvm_target
419419
);
420-
session.err(err_msg);
420+
session.dcx().err(err_msg);
421421
}
422422

423-
session.abort_if_errors();
423+
session.dcx().abort_if_errors();
424424
}
425425

426426
fn check_options(session: &Session) {
@@ -433,27 +433,27 @@ fn check_options(session: &Session) {
433433
let err_msg = format!(
434434
"Kani requires the target architecture option `min_global_align` to be 1, but it is {align}."
435435
);
436-
session.err(err_msg);
436+
session.dcx().err(err_msg);
437437
}
438438
_ => (),
439439
}
440440

441441
if session.target.options.endian != Endian::Little {
442-
session.err("Kani requires the target architecture option `endian` to be `little`.");
442+
session.dcx().err("Kani requires the target architecture option `endian` to be `little`.");
443443
}
444444

445445
if !session.overflow_checks() {
446-
session.err("Kani requires overflow checks in order to provide a sound analysis.");
446+
session.dcx().err("Kani requires overflow checks in order to provide a sound analysis.");
447447
}
448448

449449
if session.panic_strategy() != PanicStrategy::Abort {
450-
session.err(
450+
session.dcx().err(
451451
"Kani can only handle abort panic strategy (-C panic=abort). See for more details \
452452
https://github.com/model-checking/kani/issues/692",
453453
);
454454
}
455455

456-
session.abort_if_errors();
456+
session.dcx().abort_if_errors();
457457
}
458458

459459
/// Return a struct that contains information about the codegen results as expected by `rustc`.
@@ -503,8 +503,8 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf {
503503
"Failed to generate goto model:\n\tsymtab2gb failed on file {}.",
504504
input_filename.display()
505505
);
506-
tcx.sess.err(err_msg);
507-
tcx.sess.abort_if_errors();
506+
tcx.dcx().err(err_msg);
507+
tcx.dcx().abort_if_errors();
508508
};
509509
output_filename
510510
}
@@ -607,7 +607,7 @@ impl GotoCodegenResults {
607607
msg += "\nVerification will fail if one or more of these constructs is reachable.";
608608
msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \
609609
details.";
610-
tcx.sess.warn(msg);
610+
tcx.dcx().warn(msg);
611611
}
612612

613613
if !self.concurrent_constructs.is_empty() {
@@ -618,7 +618,7 @@ impl GotoCodegenResults {
618618
for (construct, locations) in self.concurrent_constructs.iter() {
619619
writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap();
620620
}
621-
tcx.sess.warn(msg);
621+
tcx.dcx().warn(msg);
622622
}
623623

624624
// Print some compilation stats.

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -360,7 +360,7 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
360360
fn_abi_request: FnAbiRequest<'tcx>,
361361
) -> ! {
362362
if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
363-
self.tcx.sess.emit_fatal(respan(span, err))
363+
self.tcx.dcx().emit_fatal(respan(span, err))
364364
} else {
365365
match fn_abi_request {
366366
FnAbiRequest::OfFnPtr { sig, extra_args } => {

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,5 +194,5 @@ impl<'tcx> GotocCtx<'tcx> {
194194
}
195195

196196
pub fn span_err(tcx: TyCtxt, span: Span, msg: String) {
197-
tcx.sess.span_err(rustc_internal::internal(span), msg);
197+
tcx.dcx().span_err(rustc_internal::internal(span), msg);
198198
}

0 commit comments

Comments
 (0)