Skip to content

Commit

Permalink
Upgrade to 2024-01-08 rust toolchain
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws committed Jan 8, 2024
1 parent b355f29 commit 6da5369
Show file tree
Hide file tree
Showing 13 changed files with 75 additions and 72 deletions.
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

0 comments on commit 6da5369

Please sign in to comment.