Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upgrade to 2024-01-08 rust toolchain #2969

Merged
merged 2 commits into from
Jan 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -649,7 +649,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_ty(actual)
),
);
self.tcx.sess.abort_if_errors();
self.tcx.dcx().abort_if_errors();
unreachable!("Rustc should have aborted already")
}

Expand Down Expand Up @@ -1303,7 +1303,7 @@ impl<'tcx> GotocCtx<'tcx> {
u64::MIN
})
};
self.tcx.sess.abort_if_errors();
self.tcx.dcx().abort_if_errors();
n
}

Expand Down Expand Up @@ -1432,7 +1432,7 @@ impl<'tcx> GotocCtx<'tcx> {
);
utils::span_err(self.tcx, span, err_msg);
}
self.tcx.sess.abort_if_errors();
self.tcx.dcx().abort_if_errors();

self.codegen_expr_to_place_stable(p, vec.index_array(index))
}
Expand Down Expand Up @@ -1472,7 +1472,7 @@ impl<'tcx> GotocCtx<'tcx> {
);
utils::span_err(self.tcx, span, err_msg);
}
self.tcx.sess.abort_if_errors();
self.tcx.dcx().abort_if_errors();

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

// Create the vector comparison expression
let e = f(arg1, arg2, ret_typ);
Expand Down Expand Up @@ -1773,7 +1773,7 @@ impl<'tcx> GotocCtx<'tcx> {
cond.ternary(t, e)
})
.collect();
self.tcx.sess.abort_if_errors();
self.tcx.dcx().abort_if_errors();
let cbmc_ret_ty = self.codegen_ty_stable(rust_ret_type);
self.codegen_expr_to_place_stable(p, Expr::vector_expr(cbmc_ret_ty, elems))
}
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
sig
}
ty::Coroutine(did, args, _) => self.coroutine_sig(did, fntyp, args),
ty::Coroutine(did, args) => self.coroutine_sig(did, fntyp, args),
_ => unreachable!("Can't get function signature of type: {:?}", fntyp),
})
}
Expand Down
22 changes: 11 additions & 11 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -417,10 +417,10 @@ fn check_target(session: &Session) {
it is {}",
&session.target.llvm_target
);
session.err(err_msg);
session.dcx().err(err_msg);
}

session.abort_if_errors();
session.dcx().abort_if_errors();
}

fn check_options(session: &Session) {
Expand All @@ -433,27 +433,27 @@ fn check_options(session: &Session) {
let err_msg = format!(
"Kani requires the target architecture option `min_global_align` to be 1, but it is {align}."
);
session.err(err_msg);
session.dcx().err(err_msg);
}
_ => (),
}

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

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

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

session.abort_if_errors();
session.dcx().abort_if_errors();
}

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

if !self.concurrent_constructs.is_empty() {
Expand All @@ -618,7 +618,7 @@ impl GotoCodegenResults {
for (construct, locations) in self.concurrent_constructs.iter() {
writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap();
}
tcx.sess.warn(msg);
tcx.dcx().warn(msg);
}

// Print some compilation stats.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -360,7 +360,7 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
fn_abi_request: FnAbiRequest<'tcx>,
) -> ! {
if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
self.tcx.sess.emit_fatal(respan(span, err))
self.tcx.dcx().emit_fatal(respan(span, err))
} else {
match fn_abi_request {
FnAbiRequest::OfFnPtr { sig, extra_args } => {
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -194,5 +194,5 @@ impl<'tcx> GotocCtx<'tcx> {
}

pub fn span_err(tcx: TyCtxt, span: Span, msg: String) {
tcx.sess.span_err(rustc_internal::internal(span), msg);
tcx.dcx().span_err(rustc_internal::internal(span), msg);
}
Loading
Loading