diff --git a/Cargo.lock b/Cargo.lock index bf34011c5f049..7660ff5c83ec9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -390,9 +390,9 @@ checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800" [[package]] name = "itertools" -version = "0.12.1" +version = "0.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ba291022dbbd398a455acf126c1e341954079855bc60dfdda641363bd6922569" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" dependencies = [ "either", ] @@ -999,9 +999,9 @@ dependencies = [ [[package]] name = "string-interner" -version = "0.15.0" +version = "0.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07f9fdfdd31a0ff38b59deb401be81b73913d76c9cc5b1aed4e1330a223420b9" +checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e" dependencies = [ "cfg-if", "hashbrown", diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index b98b09c68a582..63dfbf6781cda 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -17,7 +17,7 @@ lazy_static = "1.4.0" num = "0.4.0" num-traits = "0.2" serde = {version = "1", features = ["derive"]} -string-interner = "0.15.0" +string-interner = "0.17.0" tracing = "0.1" linear-map = {version = "1.2", features = ["serde_impl"]} diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 2ef2738020289..05002ed1eb279 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -12,7 +12,7 @@ publish = false cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } clap = { version = "4.4.11", features = ["derive", "cargo"] } home = "0.5" -itertools = "0.12" +itertools = "0.13" kani_metadata = {path = "../kani_metadata"} lazy_static = "1.4.0" num = { version = "0.4.0", optional = true } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index c8aba08ba5ed7..a7a3c43edbffb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -11,8 +11,8 @@ use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, StaticDef}; use stable_mir::mir::Operand; use stable_mir::ty::{ - Allocation, Const, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty, - TyKind, UintTy, + Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Span, + Ty, TyConst, TyConstKind, TyKind, UintTy, }; use stable_mir::{CrateDef, CrateItem}; use tracing::{debug, trace}; @@ -63,17 +63,17 @@ impl<'tcx> GotocCtx<'tcx> { ) -> Expr { let stable_const = rustc_internal::stable(constant); let stable_span = rustc_internal::stable(span); - self.codegen_const(&stable_const, stable_span) + self.codegen_const_ty(&stable_const, stable_span) } - /// Generate a goto expression that represents a constant. + /// Generate a goto expression that represents a MIR-level constant. /// /// There are two possible constants included in the body of an instance: /// - Allocated: It will have its byte representation already defined. We try to eagerly /// generate code for it as simple literals or constants if possible. Otherwise, we create /// a memory allocation for them and access them indirectly. /// - ZeroSized: These are ZST constants and they just need to match the right type. - pub fn codegen_const(&mut self, constant: &Const, span: Option) -> Expr { + pub fn codegen_const(&mut self, constant: &MirConst, span: Option) -> Expr { trace!(?constant, "codegen_constant"); match constant.kind() { ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span), @@ -90,6 +90,34 @@ impl<'tcx> GotocCtx<'tcx> { ConstantKind::Param(..) | ConstantKind::Unevaluated(..) => { unreachable!() } + ConstantKind::Ty(t) => self.codegen_const_ty(t, span), + } + } + + /// Generate a goto expression that represents a type-level constant. + /// + /// There are two possible constants included in the body of an instance: + /// - Allocated: It will have its byte representation already defined. We try to eagerly + /// generate code for it as simple literals or constants if possible. Otherwise, we create + /// a memory allocation for them and access them indirectly. + /// - ZeroSized: These are ZST constants and they just need to match the right type. + pub fn codegen_const_ty(&mut self, constant: &TyConst, span: Option) -> Expr { + trace!(?constant, "codegen_constant"); + match constant.kind() { + TyConstKind::ZSTValue(lit_ty) => { + match lit_ty.kind() { + // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) + TyKind::RigidTy(RigidTy::FnDef(def, args)) => { + self.codegen_fndef(def, &args, span) + } + _ => Expr::init_unit(self.codegen_ty_stable(*lit_ty), &self.symbol_table), + } + } + TyConstKind::Value(ty, alloc) => self.codegen_allocation(alloc, *ty, span), + TyConstKind::Bound(..) => unreachable!(), + TyConstKind::Param(..) | TyConstKind::Unevaluated(..) => { + unreachable!() + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 89a50971243b1..21185624942c7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -18,7 +18,7 @@ use cbmc::goto_program::{ use cbmc::MachineModel; use cbmc::{btree_string_map, InternString, InternedString}; use num::bigint::BigInt; -use rustc_middle::ty::{TyCtxt, VtblEntry}; +use rustc_middle::ty::{ParamEnv, TyCtxt, VtblEntry}; use rustc_smir::rustc_internal; use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; use stable_mir::abi::{Primitive, Scalar, ValueAbi}; @@ -26,7 +26,7 @@ use stable_mir::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp, }; -use stable_mir::ty::{ClosureKind, Const, IntTy, RigidTy, Size, Ty, TyKind, UintTy, VariantIdx}; +use stable_mir::ty::{ClosureKind, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy, VariantIdx}; use std::collections::BTreeMap; use tracing::{debug, trace, warn}; @@ -161,7 +161,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Codegens expressions of the type `let a = [4u8; 6];` - fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: &Const, loc: Location) -> Expr { + fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: &TyConst, loc: Location) -> Expr { let op_expr = self.codegen_operand_stable(op); let width = sz.eval_target_usize().unwrap(); op_expr.array_constant(width).with_location(loc) @@ -170,7 +170,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_rvalue_len(&mut self, p: &Place) -> Expr { let pt = self.place_ty_stable(p); match pt.kind() { - TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const(&sz, None), + TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const_ty(&sz, None), TyKind::RigidTy(RigidTy::Slice(_)) => { unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p)) .fat_ptr_goto_expr @@ -779,9 +779,10 @@ impl<'tcx> GotocCtx<'tcx> { .with_size_of_annotation(self.codegen_ty_stable(*t)), NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()), NullOp::OffsetOf(fields) => Expr::int_constant( - layout + self.tcx .offset_of_subfield( - self, + ParamEnv::reveal_all(), + layout, fields.iter().map(|(var_idx, field_idx)| { ( rustc_internal::internal(self.tcx, var_idx), @@ -814,6 +815,51 @@ impl<'tcx> GotocCtx<'tcx> { } } UnOp::Neg => self.codegen_operand_stable(e).neg(), + UnOp::PtrMetadata => { + let src_goto_expr = self.codegen_operand_stable(e); + let dst_goto_typ = self.codegen_ty_stable(res_ty); + debug!( + "PtrMetadata |{:?}| with result type |{:?}|", + src_goto_expr, dst_goto_typ + ); + if let Some(_vtable_typ) = + src_goto_expr.typ().lookup_field_type("vtable", &self.symbol_table) + { + let vtable_expr = src_goto_expr.member("vtable", &self.symbol_table); + let dst_components = + dst_goto_typ.lookup_components(&self.symbol_table).unwrap(); + assert_eq!(dst_components.len(), 2); + assert_eq!(dst_components[0].name(), "_vtable_ptr"); + assert!(dst_components[0].typ().is_pointer()); + assert_eq!(dst_components[1].name(), "_phantom"); + self.assert_is_rust_phantom_data_like(&dst_components[1].typ()); + Expr::struct_expr( + dst_goto_typ, + btree_string_map![ + ("_vtable_ptr", vtable_expr.cast_to(dst_components[0].typ())), + ( + "_phantom", + Expr::struct_expr( + dst_components[1].typ(), + [].into(), + &self.symbol_table + ) + ) + ], + &self.symbol_table, + ) + } else if let Some(len_typ) = + src_goto_expr.typ().lookup_field_type("len", &self.symbol_table) + { + assert_eq!(len_typ, dst_goto_typ); + src_goto_expr.member("len", &self.symbol_table) + } else { + unreachable!( + "fat pointer with neither vtable nor len: {:?}", + src_goto_expr + ); + } + } }, Rvalue::Discriminant(p) => { let place = @@ -1453,7 +1499,7 @@ impl<'tcx> GotocCtx<'tcx> { ) => { // Cast to a slice fat pointer. assert_eq!(src_elt_type, dst_elt_type); - let dst_goto_len = self.codegen_const(&src_elt_count, None); + let dst_goto_len = self.codegen_const_ty(&src_elt_count, None); let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap(); let dst_data_expr = if src_pointee_ty.kind().is_array() { src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer()) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index c091d0b74ead7..6d00bda5bce46 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -11,8 +11,8 @@ use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::print::FmtPrinter; use rustc_middle::ty::GenericArgsRef; use rustc_middle::ty::{ - self, AdtDef, Const, CoroutineArgs, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind, - UintTy, VariantDef, VtblEntry, + self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig, Ty, + TyCtxt, TyKind, UintTy, VariantDef, VtblEntry, }; use rustc_middle::ty::{List, TypeFoldable}; use rustc_smir::rustc_internal; diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs index e369f64beda93..16edca2a826c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs @@ -125,7 +125,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Best effort check if the struct represents a rust `std::marker::PhantomData` - fn assert_is_rust_phantom_data_like(&self, t: &Type) { + pub fn assert_is_rust_phantom_data_like(&self, t: &Type) { // TODO: A `std::marker::PhantomData` appears to be an empty struct, in the cases we've seen. // Is there something smarter we can do here? assert!(t.is_struct_like()); diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index e2617739e461e..a9c777d845060 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -633,7 +633,7 @@ fn parse_modify_values<'a>( TokenTree::Token(token, _) => { if let TokenKind::Ident(id, _) = &token.kind { let hir = tcx.hir(); - let bid = hir.body_owned_by(local_def_id); + let bid = hir.body_owned_by(local_def_id).id(); Some( hir.body_param_names(bid) .zip(mir.args_iter()) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 186bd65a7840f..9c6c7e0ec3506 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -376,6 +376,10 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { // Nothing to do here. return; } + ConstantKind::Ty(_) => { + // Nothing to do here. + return; + } }; self.collect_allocation(&allocation); } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index bd6c9be6581ac..e058c5aedc98b 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -7,7 +7,7 @@ use crate::kani_middle::find_fn_def; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::*; -use stable_mir::ty::{Const, GenericArgs, Span, Ty, UintTy}; +use stable_mir::ty::{GenericArgs, MirConst, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; @@ -80,12 +80,12 @@ impl MutableBody { } pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand { - let literal = Const::from_str(msg); + let literal = MirConst::from_str(msg); Operand::Constant(Constant { span, user_ty: None, literal }) } pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand { - let literal = Const::try_from_uint(val, uint_ty).unwrap(); + let literal = MirConst::try_from_uint(val, uint_ty).unwrap(); Operand::Constant(Constant { span, user_ty: None, literal }) } diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 893b2244f2ca7..c7c9548bd609d 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -18,7 +18,8 @@ use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruct use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; -use rustc_middle::ty::TyCtxt; +use rustc_middle::ty::{Const, TyCtxt}; +use rustc_smir::rustc_internal; use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; @@ -28,7 +29,7 @@ use stable_mir::mir::{ Statement, StatementKind, Terminator, TerminatorKind, }; use stable_mir::target::{MachineInfo, MachineSize}; -use stable_mir::ty::{AdtKind, Const, IndexedVal, RigidTy, Ty, TyKind, UintTy}; +use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Ty, TyKind, UintTy}; use stable_mir::CrateDef; use std::fmt::Debug; use strum_macros::AsRefStr; @@ -65,7 +66,7 @@ impl TransformPass for ValidValuePass { // Do not cache body.blocks().len() since it will change as we add new checks. for bb_idx in 0..new_body.blocks().len() { let Some(candidate) = - CheckValueVisitor::find_next(&new_body, bb_idx, bb_idx >= orig_len) + CheckValueVisitor::find_next(tcx, &new_body, bb_idx, bb_idx >= orig_len) else { continue; }; @@ -118,7 +119,7 @@ impl ValidValuePass { ) { let span = source.span(body.blocks()); let rvalue = Rvalue::Use(Operand::Constant(Constant { - literal: Const::from_bool(false), + literal: MirConst::from_bool(false), span, user_ty: None, })); @@ -262,7 +263,8 @@ struct UnsafeInstruction { /// - Transmute /// - MemCopy /// - Cast -struct CheckValueVisitor<'a> { +struct CheckValueVisitor<'a, 'b> { + tcx: TyCtxt<'b>, locals: &'a [LocalDecl], /// Whether we should skip the next instruction, since it might've been instrumented already. /// When we instrument an instruction, we partition the basic block, and the instruction that @@ -279,13 +281,15 @@ struct CheckValueVisitor<'a> { machine: MachineInfo, } -impl<'a> CheckValueVisitor<'a> { +impl<'a, 'b> CheckValueVisitor<'a, 'b> { fn find_next( + tcx: TyCtxt<'b>, body: &'a MutableBody, bb: BasicBlockIdx, skip_first: bool, ) -> Option { let mut visitor = CheckValueVisitor { + tcx, locals: body.locals(), skip_next: skip_first, current: SourceInstruction::Statement { idx: 0, bb }, @@ -305,7 +309,7 @@ impl<'a> CheckValueVisitor<'a> { } } -impl<'a> MirVisitor for CheckValueVisitor<'a> { +impl<'a, 'b> MirVisitor for CheckValueVisitor<'a, 'b> { fn visit_statement(&mut self, stmt: &Statement, location: Location) { if self.skip_next { self.skip_next = false; @@ -388,12 +392,10 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { match validity { Ok(ranges) if ranges.is_empty() => {} Ok(ranges) => { - let sz = Const::try_from_uint( - target_ty.layout().unwrap().shape().size.bytes() - as u128, - UintTy::Usize, - ) - .unwrap(); + let sz = rustc_internal::stable(Const::from_target_usize( + self.tcx, + target_ty.layout().unwrap().shape().size.bytes() as u64, + )); self.push_target(SourceOp::BytesValidity { target_ty, rvalue: Rvalue::Repeat(args[1].clone(), sz), diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index c99874cc42a89..10fa6775a0d98 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Body, Constant, Operand, TerminatorKind}; -use stable_mir::ty::{Const as MirConst, FnDef, RigidTy, TyKind}; +use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; use stable_mir::{CrateDef, DefId}; use std::collections::HashSet; use std::fmt::Debug; diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 6354e3777aca4..053b210babb00 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -18,7 +18,7 @@ use stable_mir::mir::{ BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, }; use stable_mir::target::MachineInfo; -use stable_mir::ty::{Const, RigidTy, TyKind}; +use stable_mir::ty::{MirConst, RigidTy, TyKind}; use std::fmt::Debug; use strum_macros::AsRefStr; use tracing::trace; @@ -82,7 +82,7 @@ impl IntrinsicGeneratorPass { Rvalue::Use(Operand::Constant(Constant { span, user_ty: None, - literal: Const::from_bool(true), + literal: MirConst::from_bool(true), })), ); let stmt = Statement { kind: assign, span }; @@ -116,7 +116,7 @@ impl IntrinsicGeneratorPass { Err(msg) => { // We failed to retrieve all the valid ranges. let rvalue = Rvalue::Use(Operand::Constant(Constant { - literal: Const::from_bool(false), + literal: MirConst::from_bool(false), span, user_ty: None, })); diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 6d8849a9f1fe8..7c4319319b8e5 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -12,7 +12,7 @@ use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, MirVisitor}; use stable_mir::mir::{Body, Constant, LocalDecl, Operand, Terminator, TerminatorKind}; -use stable_mir::ty::{Const as MirConst, FnDef, RigidTy, TyKind}; +use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; use stable_mir::CrateDef; use std::collections::HashMap; use std::fmt::Debug; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 7490dc74d65f7..d1baa70550de1 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-05-28" +channel = "nightly-2024-06-11" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/FatPointers/metadata.rs b/tests/kani/FatPointers/metadata.rs new file mode 100644 index 0000000000000..f76798e0f9f4f --- /dev/null +++ b/tests/kani/FatPointers/metadata.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(ptr_metadata)] + +struct S { + x: i32, +} + +trait T {} + +impl T for S {} + +#[kani::proof] +fn ptr_metadata() { + assert_eq!(std::ptr::metadata("foo"), 3_usize); + + let s = S { x: 42 }; + let p: &dyn T = &s; + assert_eq!(std::ptr::metadata(p).size_of(), 4_usize); + + let c: char = 'c'; + assert_eq!(std::ptr::metadata(&c), ()); +} diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index ffd08fa7eda02..4f22655157621 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -265,11 +265,11 @@ fn build_artifacts(cargo_cmd: &mut Child) -> Vec { /// Extra arguments to be given to `cargo build` while building Kani's binaries. /// Note that the following arguments are always provided: /// ```bash -/// cargo build --bins -Z unstable-options --out-dir $KANI_SYSROOT/bin/ +/// cargo build --bins -Z unstable-options --artifact-dir $KANI_SYSROOT/bin/ /// ``` pub fn build_bin>(extra_args: &[T]) -> Result { let out_dir = kani_sysroot_bin(); - let args = ["--bins", "-Z", "unstable-options", "--out-dir", out_dir.to_str().unwrap()]; + let args = ["--bins", "-Z", "unstable-options", "--artifact-dir", out_dir.to_str().unwrap()]; Command::new("cargo") .arg("build") .args(extra_args)