From a6335d0bb351faf7f310be9a0680084bc37bcb2f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 19 May 2022 13:41:58 -0700 Subject: [PATCH 1/4] Update rust toolchain to 2022-05-17 Status: Compilation succeeds but regression fails due to new intrinsic. Relevant changes: - https://github.com/rust-lang/rust/pull/95837 - https://github.com/rust-lang/rust/pull/95562 - https://github.com/rust-lang/rust/pull/96883 --- .../src/codegen_cprover_gotoc/codegen/function.rs | 3 +-- kani-compiler/src/main.rs | 1 - rust-toolchain.toml | 2 +- tools/bookrunner/librustdoc/clean/inline.rs | 6 +++--- tools/bookrunner/librustdoc/clean/mod.rs | 4 ++-- tools/bookrunner/librustdoc/clean/types.rs | 2 +- tools/bookrunner/librustdoc/clean/utils.rs | 7 +++---- 7 files changed, 11 insertions(+), 14 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 68be3a092874..431d7eac82be 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -243,9 +243,8 @@ impl<'tcx> GotocCtx<'tcx> { /// /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here) fn handle_kanitool_attributes(&mut self) { - let all_attributes = self.tcx.get_attrs(self.current_fn().instance().def_id()); + let all_attributes = self.tcx.get_attrs_unchecked(self.current_fn().instance().def_id()); let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes); - if proof_attributes.is_empty() && !other_attributes.is_empty() { self.tcx.sess.span_err( other_attributes[0].1.span, diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 03ae695f5c7f..2325a2773ee1 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -7,7 +7,6 @@ //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the //! rustc_private feature and a specific version of rustc. #![deny(warnings)] -#![feature(bool_to_option)] #![feature(crate_visibility_modifier)] #![feature(extern_types)] #![feature(nll)] diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 367b0c0ae687..8cf9ee66a46d 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-05-03" +channel = "nightly-2022-05-17" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tools/bookrunner/librustdoc/clean/inline.rs b/tools/bookrunner/librustdoc/clean/inline.rs index 84deb3a7c112..007a099374b6 100644 --- a/tools/bookrunner/librustdoc/clean/inline.rs +++ b/tools/bookrunner/librustdoc/clean/inline.rs @@ -26,7 +26,7 @@ use crate::clean::{ use crate::core::DocContext; use crate::formats::item_type::ItemType; -type Attrs<'hir> = rustc_middle::ty::Attributes<'hir>; +type Attrs<'hir> = &'hir [ast::Attribute]; /// Attempt to inline a definition into this AST. /// @@ -159,7 +159,7 @@ crate fn try_inline_glob( } fn load_attrs<'hir>(cx: &DocContext<'hir>, did: DefId) -> Attrs<'hir> { - cx.tcx.get_attrs(did) + cx.tcx.get_attrs_unchecked(did) } /// Record an external fully qualified name in the external_paths cache. @@ -685,7 +685,7 @@ crate fn record_extern_trait(cx: &mut DocContext<'_>, did: DefId) { let trait_ = clean::TraitWithExtraInfo { trait_, - is_notable: clean::utils::has_doc_flag(cx.tcx.get_attrs(did), sym::notable_trait), + is_notable: clean::utils::has_doc_flag(cx.tcx, did, sym::notable_trait), }; cx.external_traits.borrow_mut().insert(did, trait_); cx.active_extern_traits.remove(&did); diff --git a/tools/bookrunner/librustdoc/clean/mod.rs b/tools/bookrunner/librustdoc/clean/mod.rs index 4e3d0da2a81b..c9732f622843 100644 --- a/tools/bookrunner/librustdoc/clean/mod.rs +++ b/tools/bookrunner/librustdoc/clean/mod.rs @@ -19,7 +19,7 @@ use rustc_hir::def::{CtorKind, DefKind, Res}; use rustc_hir::def_id::{DefId, CRATE_DEF_INDEX, LOCAL_CRATE}; use rustc_middle::middle::resolve_lifetime as rl; use rustc_middle::ty::subst::{InternalSubsts, Subst}; -use rustc_middle::ty::{self, AdtKind, DefIdTree, Lift, Ty, TyCtxt}; +use rustc_middle::ty::{self, AdtKind, DefIdTree, EarlyBinder, Lift, Ty, TyCtxt}; use rustc_middle::{bug, span_bug}; use rustc_span::hygiene::{AstPass, MacroKind}; use rustc_span::symbol::{kw, sym, Ident, Symbol}; @@ -1544,7 +1544,7 @@ impl<'tcx> Clean for Ty<'tcx> { .tcx .explicit_item_bounds(def_id) .iter() - .map(|(bound, _)| bound.subst(cx.tcx, substs)) + .map(|(bound, _)| EarlyBinder(*bound).subst(cx.tcx, substs)) .collect::>(); let mut regions = vec![]; let mut has_sized = false; diff --git a/tools/bookrunner/librustdoc/clean/types.rs b/tools/bookrunner/librustdoc/clean/types.rs index 2634d9b04501..069b5026d5c1 100644 --- a/tools/bookrunner/librustdoc/clean/types.rs +++ b/tools/bookrunner/librustdoc/clean/types.rs @@ -197,7 +197,7 @@ impl Item { kind: ItemKind, cx: &mut DocContext<'_>, ) -> Item { - let ast_attrs = cx.tcx.get_attrs(def_id); + let ast_attrs = cx.tcx.get_attrs_unchecked(def_id); Self::from_def_id_and_attrs_and_parts(def_id, name, kind, box ast_attrs.clean(cx), cx) } diff --git a/tools/bookrunner/librustdoc/clean/utils.rs b/tools/bookrunner/librustdoc/clean/utils.rs index 75c2cbd2c76a..35b5dc915b9b 100644 --- a/tools/bookrunner/librustdoc/clean/utils.rs +++ b/tools/bookrunner/librustdoc/clean/utils.rs @@ -287,10 +287,9 @@ where /// /// This function exists because it runs on `hir::Attributes` whereas the other is a /// `clean::Attributes` method. -crate fn has_doc_flag(attrs: ty::Attributes<'_>, flag: Symbol) -> bool { - attrs.iter().any(|attr| { - attr.has_name(sym::doc) - && attr.meta_item_list().map_or(false, |l| rustc_attr::list_contains_name(&l, flag)) +crate fn has_doc_flag(tcx: TyCtxt<'_>, did: DefId, flag: Symbol) -> bool { + tcx.get_attrs(did, sym::doc).any(|attr| { + attr.meta_item_list().map_or(false, |l| rustc_attr::list_contains_name(&l, flag)) }) } From 27a00e6b0f17368246583696652af520e52d8793 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 19 May 2022 15:32:43 -0700 Subject: [PATCH 2/4] Implement new intrinsic ptr_offset_from_unsigned This new intrinsic is used in many different places in the standard library and it was failing some tests for vectors. --- cprover_bindings/src/goto_program/expr.rs | 7 ++ .../codegen_cprover_gotoc/codegen/assert.rs | 15 ++++ .../codegen/intrinsic.rs | 69 ++++++++++++++++--- .../check_invariant_violation.rs | 15 ++++ .../ptr_offset_from_unsigned/expected | 1 + .../check_unsigned_ptr_offset_from.rs | 31 +++++++++ 6 files changed, 127 insertions(+), 11 deletions(-) create mode 100644 tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs create mode 100644 tests/expected/intrinsics/ptr_offset_from_unsigned/expected create mode 100644 tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 1ab3c595ab79..ccd30771a6ac 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -1221,6 +1221,13 @@ impl Expr { self.lt(typ.zero()) } + /// `self >= 0` + pub fn is_non_negative(self) -> Self { + assert!(self.typ.is_numeric()); + let typ = self.typ.clone(); + self.ge(typ.zero()) + } + /// `self == 0` pub fn is_zero(self) -> Self { assert!(self.typ.is_numeric()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index d5032b0747fa..2a04989681bf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -83,6 +83,21 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::assert(cond, property_name, message, loc) } + pub fn codegen_assert_assume( + &self, + cond: Expr, + property_class: PropertyClass, + message: &str, + loc: Location, + ) -> Stmt { + assert!(cond.typ().is_bool()); + let property_name = property_class.as_str(); + Stmt::block( + vec![Stmt::assert(cond.clone(), property_name, message, loc), Stmt::assume(cond, loc)], + loc, + ) + } + pub fn codegen_assert_false( &self, property_class: PropertyClass, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index ac8d805e2d80..421da67d66ab 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -4,7 +4,7 @@ use super::typ::pointee_type; use super::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; +use cbmc::goto_program::{ArithmeticOverflowResult, BuiltinFn, Expr, Location, Stmt, Type}; use rustc_middle::mir::{BasicBlock, Operand, Place}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Ty}; @@ -551,6 +551,7 @@ impl<'tcx> GotocCtx<'tcx> { "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq), "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc), + "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, p, loc), "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc), "rintf32" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" @@ -994,33 +995,79 @@ impl<'tcx> GotocCtx<'tcx> { /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html fn codegen_ptr_offset_from( &mut self, - mut fargs: Vec, + fargs: Vec, p: &Place<'tcx>, loc: Location, ) -> Stmt { - let dst_ptr = fargs.remove(0); - let src_ptr = fargs.remove(0); - - // Compute the offset with standard substraction using `isize` - let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t()); - let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); - let offset = cast_dst_ptr.sub_overflow(cast_src_ptr); + let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); // Check that computing `offset` in bytes would not overflow an `isize` // These checks may allow a wrapping-around behavior in CBMC: // https://github.com/model-checking/kani/issues/1150 let overflow_check = self.codegen_assert( - offset.overflowed.not(), + offset_overflow.overflowed.not(), PropertyClass::ArithmeticOverflow, "attempt to compute offset in bytes which would overflow an `isize`", loc, ); // Re-compute the offset with standard substraction (no casts this time) - let offset_expr = self.codegen_expr_to_place(p, dst_ptr.sub(src_ptr)); + let offset_expr = self.codegen_expr_to_place(p, offset_expr); Stmt::block(vec![overflow_check, offset_expr], loc) } + /// ptr_offset_from_unsigned returns the offset between two pointers where the order is known. + /// The logic is similar to ptr_offset_from but the return value is a usize. + /// See https://github.com/rust-lang/rust/issues/95892 for more details + fn codegen_ptr_offset_from_unsigned( + &mut self, + fargs: Vec, + p: &Place<'tcx>, + loc: Location, + ) -> Stmt { + let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); + + // Check that computing `offset` in bytes would not overflow an `isize` + // These checks may allow a wrapping-around behavior in CBMC: + // https://github.com/model-checking/kani/issues/1150 + let overflow_check = self.codegen_assert( + offset_overflow.overflowed.not(), + PropertyClass::ArithmeticOverflow, + "attempt to compute offset in bytes which would overflow an `isize`", + loc, + ); + + let non_negative_check = self.codegen_assert_assume( + offset_overflow.result.is_non_negative(), + PropertyClass::KaniCheck, + "safety condition violated: computing unsigned offset with negative distance", + loc, + ); + + // Re-compute the offset with standard substraction (no casts this time) + let offset_expr = self.codegen_expr_to_place(p, offset_expr.cast_to(Type::size_t())); + Stmt::block(vec![non_negative_check, overflow_check, offset_expr], loc) + } + + /// Both ptr_offset_from and ptr_offset_from_unsigned returns the offset between two pointers. + /// This function implements the common logic between them. + fn codegen_ptr_offset_from_expr( + &mut self, + mut fargs: Vec, + ) -> (Expr, ArithmeticOverflowResult) { + let dst_ptr = fargs.remove(0); + let src_ptr = fargs.remove(0); + + // Compute the offset with standard substraction using `isize` + let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t()); + let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); + let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr); + + // Re-compute the offset with standard substraction (no casts this time) + let ptr_offset_expr = dst_ptr.sub(src_ptr); + (ptr_offset_expr, offset_overflow) + } + /// A transmute is a bitcast from the argument type to the return type. /// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html /// diff --git a/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs b/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs new file mode 100644 index 000000000000..87e96272315c --- /dev/null +++ b/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(core_intrinsics)] +use std::intrinsics::ptr_offset_from_unsigned; + +#[kani::proof] +fn check_failure() { + let a = [0; 5]; + let ptr0: *const i32 = &a[0]; + let ptr1: *const i32 = &a[1]; + unsafe { + let _distance = ptr_offset_from_unsigned(ptr0, ptr1); + } +} diff --git a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected new file mode 100644 index 000000000000..99134ae0d940 --- /dev/null +++ b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected @@ -0,0 +1 @@ +Failed Checks: safety condition violated: computing unsigned offset with negative distance diff --git a/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs b/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs new file mode 100644 index 000000000000..9e91c09208eb --- /dev/null +++ b/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(core_intrinsics)] +use std::intrinsics::ptr_offset_from_unsigned; + +#[kani::proof] +fn check_distance_i32() { + let a = [0; 5]; + let ptr0: *const i32 = &a[0]; + let ptr1: *const i32 = &a[1]; + let ptr2: *const i32 = &a[2]; + unsafe { + assert_eq!(ptr_offset_from_unsigned(ptr2, ptr0), 2); + assert_eq!(ptr_offset_from_unsigned(ptr1, ptr0), 1); + assert_eq!(ptr_offset_from_unsigned(ptr2, ptr2), 0); + } +} + +#[kani::proof] +fn check_distance_i64() { + let a = [0i64; 5]; + let ptr0: *const i64 = &a[0]; + let ptr1: *const i64 = &a[1]; + let ptr2: *const i64 = &a[2]; + unsafe { + assert_eq!(ptr_offset_from_unsigned(ptr2, ptr0), 2); + assert_eq!(ptr_offset_from_unsigned(ptr1, ptr0), 1); + assert_eq!(ptr_offset_from_unsigned(ptr1, ptr1), 0); + } +} From f331ccf6d4cc3feafe55b28b74ecb53a77c30328 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 20 May 2022 14:11:37 -0700 Subject: [PATCH 3/4] Apply suggestions from code review Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 421da67d66ab..3a901b3157da 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1016,8 +1016,8 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(vec![overflow_check, offset_expr], loc) } - /// ptr_offset_from_unsigned returns the offset between two pointers where the order is known. - /// The logic is similar to ptr_offset_from but the return value is a usize. + /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known. + /// The logic is similar to `ptr_offset_from` but the return value is a `usize`. /// See https://github.com/rust-lang/rust/issues/95892 for more details fn codegen_ptr_offset_from_unsigned( &mut self, @@ -1049,7 +1049,7 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(vec![non_negative_check, overflow_check, offset_expr], loc) } - /// Both ptr_offset_from and ptr_offset_from_unsigned returns the offset between two pointers. + /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers. /// This function implements the common logic between them. fn codegen_ptr_offset_from_expr( &mut self, From ff07c332e719d70e4a0962706c7473929aacb689 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 24 May 2022 11:02:19 -0700 Subject: [PATCH 4/4] Address PR comments - Fix order of checks. - Improve error message. - Add comments to the new tests. --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 8 +++----- .../ptr_offset_from_unsigned/check_invariant_violation.rs | 2 ++ .../expected/intrinsics/ptr_offset_from_unsigned/expected | 2 +- .../check_unsigned_ptr_offset_from.rs | 1 + 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3a901b3157da..a1d3c0d8b44c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1011,7 +1011,6 @@ impl<'tcx> GotocCtx<'tcx> { loc, ); - // Re-compute the offset with standard substraction (no casts this time) let offset_expr = self.codegen_expr_to_place(p, offset_expr); Stmt::block(vec![overflow_check, offset_expr], loc) } @@ -1030,7 +1029,7 @@ impl<'tcx> GotocCtx<'tcx> { // Check that computing `offset` in bytes would not overflow an `isize` // These checks may allow a wrapping-around behavior in CBMC: // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert( + let overflow_check = self.codegen_assert_assume( offset_overflow.overflowed.not(), PropertyClass::ArithmeticOverflow, "attempt to compute offset in bytes which would overflow an `isize`", @@ -1040,13 +1039,12 @@ impl<'tcx> GotocCtx<'tcx> { let non_negative_check = self.codegen_assert_assume( offset_overflow.result.is_non_negative(), PropertyClass::KaniCheck, - "safety condition violated: computing unsigned offset with negative distance", + "attempt to compute unsigned offset with negative distance", loc, ); - // Re-compute the offset with standard substraction (no casts this time) let offset_expr = self.codegen_expr_to_place(p, offset_expr.cast_to(Type::size_t())); - Stmt::block(vec![non_negative_check, overflow_check, offset_expr], loc) + Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc) } /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers. diff --git a/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs b/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs index 87e96272315c..0e08e543dfea 100644 --- a/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs +++ b/tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs @@ -1,5 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani correctly detects a safety violation when user tries to invoke the +//! `ptr_offset_from_unsigned` intrinsic in the wrong order. #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from_unsigned; diff --git a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected index 99134ae0d940..8a893dea24be 100644 --- a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected +++ b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected @@ -1 +1 @@ -Failed Checks: safety condition violated: computing unsigned offset with negative distance +Failed Checks: attempt to compute unsigned offset with negative distance diff --git a/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs b/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs index 9e91c09208eb..c688ba6e3ac7 100644 --- a/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs +++ b/tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! Checks that the ptr_offset_from_unsigned intrinsic returns the expected results. #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from_unsigned;