Toolchain upgrade to nightly-2025-04-08 failed

[github-actions]

Updating Rust toolchain from nightly-2025-04-07 to nightly-2025-04-08 requires source changes.
The failed automated run can be found here.
Please review the changes at https://github.com/rust-lang/rust from rust-lang/rust@2fa8b11 up to rust-lang/rust@e643f59. The log for this commit range is:
rust-lang/rust@e643f59f6d Auto merge of #139482 - Zalathar:rollup-h2ht1y6, r=Zalathar
rust-lang/rust@6e0b67419c Rollup merge of #139466 - compiler-errors:trivial-incr-tainting, r=oli-obk
rust-lang/rust@5863b426b9 Rollup merge of #139465 - EnzymeAD:autodiff-sret, r=oli-obk
rust-lang/rust@0178254f46 Rollup merge of #139461 - compiler-errors:significant-drop-span, r=oli-obk
rust-lang/rust@9209c5eb60 Rollup merge of #139455 - Skgland:remove_rust-intrinsic_ABI, r=oli-obk
rust-lang/rust@ddf099ff4e Rollup merge of #139397 - Zalathar:virtual, r=jieyouxu
rust-lang/rust@f4c429fde5 Rollup merge of #139365 - Bryanskiy:leak-perf, r=lcnr
rust-lang/rust@27c6e40755 Rollup merge of #139112 - m-ou-se:super-let, r=lcnr
rust-lang/rust@9955b7634d Rollup merge of #139108 - Nadrieril:simplify-expandedconstant, r=oli-obk
rust-lang/rust@82df6229b6 Rollup merge of #139035 - nnethercote:PatKind-Missing, r=oli-obk
rust-lang/rust@ca5bea3ebb move old tests, add sret test
rust-lang/rust@d6467d34ae handle sret for scalar autodiff
rust-lang/rust@4322b6e97d coverage: Build the CGU's global file table as late as possible
rust-lang/rust@8fb32ab8e5 Auto merge of #139473 - Kobzol:rollup-ycksn9b, r=Kobzol
rust-lang/rust@58ad76313f Rollup merge of #139467 - compiler-errors:more-trivial-tweaks, r=oli-obk
rust-lang/rust@1b8dbda9c7 Rollup merge of #139456 - calebcartwright:style-let-chains-final, r=joshtriplett
rust-lang/rust@501235451c Rollup merge of #139431 - beetrees:no-llvm-18, r=jieyouxu
rust-lang/rust@f4177f4bde Rollup merge of #139426 - jackh726:rust-analyzer-next-solver-new, r=lcnr
rust-lang/rust@5a43d92382 Rollup merge of #138314 - haenoe:autodiff-inner-function, r=ZuseZ4
rust-lang/rust@c51c448fae More trivial tweaks
rust-lang/rust@d111aa87f1 Trivial tweaks to stop tracking source span directly
rust-lang/rust@b9856b6e40 Auto merge of #138766 - Zalathar:unused-fn, r=SparrowLii
rust-lang/rust@ee07e3f83f doc(style): add let-chain rules
rust-lang/rust@25a615bf82 Auto merge of #138951 - jwnrt:alloc-raw-vec-strict-prov, r=Noratrieb
rust-lang/rust@c8649a31a8 Stop calling source_span query in significant drop order code
rust-lang/rust@bf69443a9f refactor: simplify function-info gathering
rust-lang/rust@7dd57f085c update/bless tests
rust-lang/rust@6dfb29624c update docs
rust-lang/rust@51b51b51d7 remove rust-analyser support for extern "rust-intrinsic" blocks
rust-lang/rust@63e825e52a feat: apply autodiff macro twice to inner function
rust-lang/rust@5eb535c568 remove compiler support for extern "rust-intrinsic" blocks
rust-lang/rust@72091edcc4 feat: add test to validate autodiff macro expansion
rust-lang/rust@13bf79cd87 fix usage of autodiff macro with inner functions
rust-lang/rust@cd4453fdba Explicitly depend on ena in rustc_type_ir and make the UnifyKey and UnifyValue imports non-nightly
rust-lang/rust@d912c03525 Reuse parent_args
rust-lang/rust@961c7463d8 Add the inline const type annotation in pattern lowering
rust-lang/rust@50e10b37c0 Tweak lower_pat_expr
rust-lang/rust@090d76497f Remove the is_inline field from PatKind::ExpandedConstant
rust-lang/rust@de57c0515d Let const_to_pat handle the ExpandedConstant wrapping
rust-lang/rust@b3c40cf374 coverage: Deal with unused functions and their names in one place
rust-lang/rust@75135aaf19 coverage: Extract module mapgen::unused for handling unused functions
rust-lang/rust@3aac9a37a5 Remove LLVM 18 inline ASM span fallback
rust-lang/rust@ccbef74fc5 Add tests for super let.
rust-lang/rust@0522ed059d Default auto traits: fix perf
rust-lang/rust@6c3417dd15 fixup! Implement super let.
rust-lang/rust@b9babad927 Add feature gate test for cfg'd out super let.
rust-lang/rust@3e6cc7689d Boolean hate.
rust-lang/rust@f02e278639 Fix typo in pretty printing super let.
rust-lang/rust@3123df8ef0 Implement super let.
rust-lang/rust@909f449247 Remove kw::Extra checks that are no longer necessary.
rust-lang/rust@9f089e080c Add {ast,hir,thir}::PatKind::Missing variants.
rust-lang/rust@aadfd810f6 Swap usize -> ptr transmute for strict_pov API
rust-lang/rust@78e9621390 Pass Alignment for RawVecInner::new_in
rust-lang/rust@d872845eae Expose Unique::from<NonNull> in const internally

[zhassan-aws]

The following regression fails with this toolchain upgrade: tests/kani/FunctionContracts/modify_slice_elem.rs.

This is a minimized test that also fails:

#[kani::ensures(|_| true)]
fn modify_slice(slice: &[u32]) {}

#[kani::proof_for_contract(modify_slice)]
fn check_modify_slice() {
    let data = Vec::new();
    modify_slice(&data)
}

$ kani modify_slice_elem.rs -Zfunction-contracts
...
SUMMARY:
 ** 1 of 112 failed (3 unreachable)
Failed Checks: misaligned pointer to reference cast: address must be a multiple of its type's alignment
 File: "/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs", line 138, in std::slice::from_raw_parts::<'_, u32>

VERIFICATION:- FAILED

[zhassan-aws]

This one also fails:

#[kani::ensures(|_| true)]
fn modify_slice() {}

#[kani::proof_for_contract(modify_slice)]
fn check_modify_slice() {
    let data = Vec::new();
    let slice: &[u32] = &data;
    modify_slice();
}

SUMMARY:
 ** 1 of 112 failed (3 unreachable)
Failed Checks: misaligned pointer to reference cast: address must be a multiple of its type's alignment
 File: "/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs", line 138, in std::slice::from_raw_parts::<'_, u32>

VERIFICATION:- FAILED

What is really mysterious is that the same test doesn't fail without function contracts:

#[kani::ensures(|_| true)]
fn modify_slice() {}

//#[kani::proof_for_contract(modify_slice)]
#[kani::proof]
fn check_modify_slice() {
    let data = Vec::new();
    let slice: &[u32] = &data;
    modify_slice();
}

SUMMARY:
 ** 0 of 84 failed (3 unreachable)

VERIFICATION:- SUCCESSFUL

[remi-delmas-3000]

@zhassan-aws Would you be able to

• print the Rust wrapper function generated by Kani for this one ?
• ask CBMC generate a stack trace for that counter example ?
• provide the GOTO file generated for that example ?

This is a Rust raw pointer error, so I suspect that it is due to the Rust contract wrapper function, not to the instrumentation that happens at GOTO level for contracts (it does not generate rust constructs).

[zhassan-aws]

The Rust wrapper can be generated by setting RUSTFLAGS=-Zunpretty=expanded when running Kani. Here's the output:

#![feature(prelude_import)]
#![no_std]


#![feature(register_tool)]
#![register_tool(kanitool)]
#[prelude_import]
use ::std::prelude::rust_2015::*;
#[macro_use]
extern crate std;
extern crate kani;
#[kanitool::recursion_check = "__kani_recursion_check_modify_slice"]
#[kanitool::checked_with = "__kani_check_modify_slice"]
#[kanitool::replaced_with = "__kani_replace_modify_slice"]
#[kanitool::asserted_with = "__kani_assert_modify_slice"]
#[kanitool::modifies_wrapper = "__kani_modifies_modify_slice"]
fn modify_slice() {
    #[inline(never)]
    #[kanitool::fn_marker = "kani_register_contract"]
    const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
        kani::panic("internal error: entered unreachable code: ")
    }
    #[inline(never)]
    #[kanitool::fn_marker = "kani_contract_mode"]
    const fn kani_contract_mode() -> kani::internal::Mode {
        kani::internal::ORIGINAL
    }
    let kani_contract_mode = kani_contract_mode();
    match kani_contract_mode {
        kani::internal::RECURSION_CHECK => {
            #[kanitool::is_contract_generated(recursion_check)]
            #[allow(dead_code, unused_variables, unused_mut)]
            let mut __kani_recursion_check_modify_slice =
                ||
                    {
                        #[kanitool::recursion_tracker]
                        static mut REENTRY: bool = false;
                        if unsafe { REENTRY } {
                                #[kanitool::is_contract_generated(replace)]
                                #[allow(dead_code, unused_variables, unused_mut)]
                                let mut __kani_replace_modify_slice =
                                    ||
                                        {
                                            let result_kani_internal: () = kani::any_modifies();
                                            kani::assume(kani::internal::apply_closure(|_| true,
                                                    &result_kani_internal));
                                            result_kani_internal
                                        };
                                __kani_replace_modify_slice()
                            } else {
                               unsafe { REENTRY = true };
                               #[kanitool::is_contract_generated(check)]
                               #[allow(dead_code, unused_variables, unused_mut)]
                               let mut __kani_check_modify_slice =
                                   ||
                                       {
                                           let _wrapper_arg = ();
                                           #[kanitool::is_contract_generated(wrapper)]
                                           #[allow(dead_code, unused_variables, unused_mut)]
                                           let mut __kani_modifies_modify_slice = |_wrapper_arg| {};
                                           let result_kani_internal: () =
                                               __kani_modifies_modify_slice(_wrapper_arg);
                                           kani::assert(kani::internal::apply_closure(|_| true,
                                                   &result_kani_internal), "|_| true");
                                           result_kani_internal
                                       };
                               let result_kani_internal = __kani_check_modify_slice();
                               unsafe { REENTRY = false };
                               result_kani_internal
                           }
                    };
            ;
            kani_register_contract(__kani_recursion_check_modify_slice)
        }
        kani::internal::REPLACE => {
            #[kanitool::is_contract_generated(replace)]
            #[allow(dead_code, unused_variables, unused_mut)]
            let mut __kani_replace_modify_slice =
                ||
                    {
                        let result_kani_internal: () = kani::any_modifies();
                        kani::assume(kani::internal::apply_closure(|_| true,
                                &result_kani_internal));
                        result_kani_internal
                    };
            ;
            kani_register_contract(__kani_replace_modify_slice)
        }
        kani::internal::SIMPLE_CHECK => {
            #[kanitool::is_contract_generated(check)]
            #[allow(dead_code, unused_variables, unused_mut)]
            let mut __kani_check_modify_slice =
                ||
                    {
                        let _wrapper_arg = ();
                        #[kanitool::is_contract_generated(wrapper)]
                        #[allow(dead_code, unused_variables, unused_mut)]
                        let mut __kani_modifies_modify_slice = |_wrapper_arg| {};
                        let result_kani_internal: () =
                            __kani_modifies_modify_slice(_wrapper_arg);
                        kani::assert(kani::internal::apply_closure(|_| true,
                                &result_kani_internal), "|_| true");
                        result_kani_internal
                    };
            ;
            kani_register_contract(__kani_check_modify_slice)
        }
        kani::internal::ASSERT => {
            #[kanitool::is_contract_generated(assert)]
            #[allow(dead_code, unused_variables, unused_mut)]
            let mut __kani_assert_modify_slice =
                ||
                    {
                        let mut body_wrapper = || {};
                        let result_kani_internal: () = body_wrapper();
                        kani::assert(kani::internal::apply_closure(|_| true,
                                &result_kani_internal), "|_| true");
                        result_kani_internal
                    };
            ;
            kani_register_contract(__kani_assert_modify_slice)
        }
        _ => {}
    }
}
#[allow(dead_code)]
#[kanitool::proof_for_contract = "modify_slice"]
fn check_modify_slice() {
    kani::internal::init_contracts();
    let data = Vec::new();
    let slice: &[u32] = &data;
    modify_slice();
}

[zhassan-aws]

Here's the trace:

CBMC Trace

$ kani test.rs --no-assertion-reach-checks --output-format=old -Zfunction-contracts -Zunstable-options --cbmc-args --trace
Kani Rust Verifier 0.61.0 (standalone)
warning: target feature `x87` must be enabled to ensure that the ABI of the current target can be implemented correctly
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>

warning: target feature `sse2` must be enabled to ensure that the ABI of the current target can be implemented correctly
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>

warning: unused variable: `slice`
 --> test.rs:9:9
  |
9 |     let slice: &[u32] = &data;
  |         ^^^^^ help: if this is intentional, prefix it with an underscore: `_slice`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: 4 warnings emitted

Checking harness check_modify_slice...
CBMC version 6.5.0 (cbmc-6.5.0) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/examples/iss4009/test__RNvCs8RDeLTht6ug_4test18check_modify_slice.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.0556542s
size of program expression: 1817 steps
slicing removed 1067 assignments
Generated 63 VCC(s), 15 remaining after simplification
Runtime Postprocess Equation: 0.000277847s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00713463s
Running propositional reduction
Post-processing
Runtime Post-process: 5.89e-06s
Solving with CaDiCaL 2.0.0
7284 variables, 12022 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000496663s
Runtime decision procedure: 0.00785153s
Building error trace
Running propositional reduction
Solving with CaDiCaL 2.0.0
7285 variables, 12023 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 3.9171e-05s
Runtime decision procedure: 9.2813e-05s

** Results:
/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::current_memory
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.1] line 527 dereference failure: pointer NULL in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.2] line 527 dereference failure: pointer invalid in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.3] line 527 dereference failure: deallocated dynamic object in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.4] line 527 dereference failure: dead object in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.5] line 527 dereference failure: pointer outside object bounds in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.6] line 527 dereference failure: invalid integer address in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.assigns.1] line 528 Check that *((unsigned long int *)((unsigned char *)&temp_1 + 8)) is assignable: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.19] line 528 dereference failure: dead object in *((unsigned long int *)((unsigned char *)&temp_1 + 8)): SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.7] line 535 dereference failure: pointer NULL in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.8] line 535 dereference failure: pointer invalid in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.9] line 535 dereference failure: deallocated dynamic object in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.10] line 535 dereference failure: dead object in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.11] line 535 dereference failure: pointer outside object bounds in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.12] line 535 dereference failure: invalid integer address in self->cap: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.13] line 537 dereference failure: pointer NULL in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.14] line 537 dereference failure: pointer invalid in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.15] line 537 dereference failure: deallocated dynamic object in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.16] line 537 dereference failure: dead object in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.17] line 537 dereference failure: pointer outside object bounds in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::current_memory.pointer_dereference.18] line 537 dereference failure: invalid integer address in self->ptr: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::deallocate
[alloc::raw_vec::RawVecInner::deallocate.unreachable.1] line 754 unreachable code: SUCCESS
[alloc::raw_vec::RawVecInner::deallocate.pointer_dereference.1] line 755 dereference failure: dead object in *((unsigned long int *)((unsigned char *)&var_3 + 8)): SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32>
[alloc::raw_vec::RawVecInner::non_null::<u32>.pointer_dereference.1] line 512 dereference failure: pointer NULL in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::non_null::<u32>.pointer_dereference.2] line 512 dereference failure: pointer invalid in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::non_null::<u32>.pointer_dereference.3] line 512 dereference failure: deallocated dynamic object in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::non_null::<u32>.pointer_dereference.4] line 512 dereference failure: dead object in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::non_null::<u32>.pointer_dereference.5] line 512 dereference failure: pointer outside object bounds in self->ptr: SUCCESS
[alloc::raw_vec::RawVecInner::non_null::<u32>.pointer_dereference.6] line 512 dereference failure: invalid integer address in self->ptr: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function <std::vec::Vec<u32> as std::ops::Drop>::drop
[<std::vec::Vec<u32> as std::ops::Drop>::drop.pointer_dereference.1] line 3798 dereference failure: pointer NULL in self->len: SUCCESS
[<std::vec::Vec<u32> as std::ops::Drop>::drop.pointer_dereference.2] line 3798 dereference failure: pointer invalid in self->len: SUCCESS
[<std::vec::Vec<u32> as std::ops::Drop>::drop.pointer_dereference.3] line 3798 dereference failure: deallocated dynamic object in self->len: SUCCESS
[<std::vec::Vec<u32> as std::ops::Drop>::drop.pointer_dereference.4] line 3798 dereference failure: dead object in self->len: SUCCESS
[<std::vec::Vec<u32> as std::ops::Drop>::drop.pointer_dereference.5] line 3798 dereference failure: pointer outside object bounds in self->len: SUCCESS
[<std::vec::Vec<u32> as std::ops::Drop>::drop.pointer_dereference.6] line 3798 dereference failure: invalid integer address in self->len: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::as_slice
[std::vec::Vec::<u32>::as_slice.pointer_dereference.1] line 1600 dereference failure: pointer NULL in self->len: SUCCESS
[std::vec::Vec::<u32>::as_slice.pointer_dereference.2] line 1600 dereference failure: pointer invalid in self->len: SUCCESS
[std::vec::Vec::<u32>::as_slice.pointer_dereference.3] line 1600 dereference failure: deallocated dynamic object in self->len: SUCCESS
[std::vec::Vec::<u32>::as_slice.pointer_dereference.4] line 1600 dereference failure: dead object in self->len: SUCCESS
[std::vec::Vec::<u32>::as_slice.pointer_dereference.5] line 1600 dereference failure: pointer outside object bounds in self->len: SUCCESS
[std::vec::Vec::<u32>::as_slice.pointer_dereference.6] line 1600 dereference failure: invalid integer address in self->len: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs function std::alloc::Layout::align
[std::alloc::Layout::align.pointer_dereference.1] line 161 dereference failure: pointer NULL in self->align: SUCCESS
[std::alloc::Layout::align.pointer_dereference.2] line 161 dereference failure: pointer invalid in self->align: SUCCESS
[std::alloc::Layout::align.pointer_dereference.3] line 161 dereference failure: deallocated dynamic object in self->align: SUCCESS
[std::alloc::Layout::align.pointer_dereference.4] line 161 dereference failure: dead object in self->align: SUCCESS
[std::alloc::Layout::align.pointer_dereference.5] line 161 dereference failure: pointer outside object bounds in self->align: SUCCESS
[std::alloc::Layout::align.pointer_dereference.6] line 161 dereference failure: invalid integer address in self->align: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs function std::alloc::Layout::is_size_align_valid
[std::alloc::Layout::is_size_align_valid.unreachable.1] line 78 unreachable code: SUCCESS
[std::alloc::Layout::is_size_align_valid.pointer_dereference.1] line 79 dereference failure: dead object in *((unsigned long int *)&var_4): SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs function std::alloc::Layout::max_size_for_align
[std::alloc::Layout::max_size_for_align.arithmetic_overflow.1] line 105 attempt to compute `unchecked_sub` which would overflow: SUCCESS
[std::alloc::Layout::max_size_for_align.assertion.1] line 105 attempt to add with overflow: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs function std::alloc::Layout::size
[std::alloc::Layout::size.pointer_dereference.1] line 149 dereference failure: pointer NULL in self->size: SUCCESS
[std::alloc::Layout::size.pointer_dereference.2] line 149 dereference failure: pointer invalid in self->size: SUCCESS
[std::alloc::Layout::size.pointer_dereference.3] line 149 dereference failure: deallocated dynamic object in self->size: SUCCESS
[std::alloc::Layout::size.pointer_dereference.4] line 149 dereference failure: dead object in self->size: SUCCESS
[std::alloc::Layout::size.pointer_dereference.5] line 149 dereference failure: pointer outside object bounds in self->size: SUCCESS
[std::alloc::Layout::size.pointer_dereference.6] line 149 dereference failure: invalid integer address in self->size: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs function std::fmt::Arguments::<'_>::new_const::<1>
[std::fmt::Arguments::<'_>::new_const::<1>.assigns.1] line 632 Check that *((unsigned char **)&temp_0) is assignable: SUCCESS
[std::fmt::Arguments::<'_>::new_const::<1>.pointer_dereference.1] line 632 dereference failure: dead object in *((unsigned char **)&temp_0): SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/intrinsics/mod.rs function core::panicking::panic_nounwind_fmt
[core::panicking::panic_nounwind_fmt.sanity_check.1] line 3193 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/uint_macros.rs function core::num::<impl usize>::unchecked_mul
[core::num::<impl usize>::unchecked_mul.arithmetic_overflow.1] line 990 attempt to compute `unchecked_mul` which would overflow: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic/location.rs function std::panic::Location::<'_>::caller
[std::panic::Location::<'_>::caller.unsupported_construct.1] line 89 caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs function core::panicking::panic_nounwind
[core::panicking::panic_nounwind.sanity_check.1] line 218 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs function core::panicking::panic_nounwind_fmt::runtime
[core::panicking::panic_nounwind_fmt::runtime.sanity_check.1] line 117 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs function std::rt::panic_fmt
[std::rt::panic_fmt.unsupported_construct.1] line 64 call to foreign "Rust" function `_RNvCsfE49cSrwkQk_7___rustc17rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::as_usize
[std::ptr::Alignment::as_usize.assume.1] line 92 Rust intrinsic assumption failed: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::new
[std::ptr::Alignment::new.assigns.1] line 62 Check that *((unsigned long int *)&temp_1) is assignable: SUCCESS
[std::ptr::Alignment::new.pointer_dereference.1] line 62 dereference failure: dead object in *((unsigned long int *)&temp_1): SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs function std::ptr::const_ptr::<impl *const ()>::is_aligned_to
[std::ptr::const_ptr::<impl *const ()>::is_aligned_to.assertion.2] line 1475 This is a placeholder message; Kani doesn't support message formatted at runtime: SUCCESS
[std::ptr::const_ptr::<impl *const ()>::is_aligned_to.assertion.1] line 1478 attempt to subtract with overflow: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::drop_in_place::<alloc::raw_vec::RawVec<u32>>
[std::ptr::drop_in_place::<alloc::raw_vec::RawVec<u32>>.safety_check.1] line 524 misaligned pointer to reference cast: address must be a multiple of its type's alignment: SUCCESS
[std::ptr::drop_in_place::<alloc::raw_vec::RawVec<u32>>.safety_check.2] line 524 dereference failure: pointer invalid: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::drop_in_place::<std::vec::Vec<u32>>
[std::ptr::drop_in_place::<std::vec::Vec<u32>>.safety_check.1] line 524 misaligned pointer to reference cast: address must be a multiple of its type's alignment: SUCCESS
[std::ptr::drop_in_place::<std::vec::Vec<u32>>.safety_check.2] line 524 dereference failure: pointer invalid: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs function std::slice::from_raw_parts::<'_, u32>
[std::slice::from_raw_parts::<'_, u32>.safety_check.1] line 138 misaligned pointer to reference cast: address must be a multiple of its type's alignment: FAILURE
[std::slice::from_raw_parts::<'_, u32>.safety_check.2] line 138 dereference failure: pointer invalid: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs function core::num::<impl usize>::unchecked_mul::precondition_check
[core::num::<impl usize>::unchecked_mul::precondition_check.sanity_check.1] line 68 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs function core::ub_checks::is_valid_allocation_size
[core::ub_checks::is_valid_allocation_size.arithmetic_overflow.1] line 134 attempt to divide by zero: SUCCESS
[core::ub_checks::is_valid_allocation_size.assertion.1] line 134 attempt to divide by zero: SUCCESS
[core::ub_checks::is_valid_allocation_size.division-by-zero.1] line 134 division by zero in var_4 / size: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs function std::alloc::Layout::from_size_align_unchecked::precondition_check
[std::alloc::Layout::from_size_align_unchecked::precondition_check.sanity_check.1] line 68 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs function std::ptr::Alignment::new_unchecked::precondition_check
[std::ptr::Alignment::new_unchecked::precondition_check.sanity_check.1] line 68 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs function std::slice::from_raw_parts::precondition_check
[std::slice::from_raw_parts::precondition_check.sanity_check.1] line 68 Kani-internal sanity check: Unexpected return from Never function. Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

/home/ubuntu/git/kani/library/kani/kani_lib.c function __rust_dealloc
[__rust_dealloc.assertion.1] line 85 Alignment is power of two: SUCCESS
[__rust_dealloc.assertion.2] line 87 rust_dealloc must be called on an object whose allocated size matches its layout: SUCCESS
[__rust_dealloc.precondition_instance.1] line 89 free argument must be NULL or valid pointer: SUCCESS
[__rust_dealloc.precondition_instance.2] line 89 free argument must be dynamic object: SUCCESS
[__rust_dealloc.precondition_instance.3] line 89 free argument has offset zero: SUCCESS
[__rust_dealloc.precondition_instance.4] line 89 double free: SUCCESS
[__rust_dealloc.precondition_instance.5] line 89 free called for new[] object: SUCCESS
[__rust_dealloc.precondition_instance.6] line 89 free called for stack-allocated object: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_make_invalid_pointer
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.1] line 1186 dereference failure: pointer NULL in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.2] line 1186 dereference failure: pointer invalid in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.3] line 1186 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.4] line 1186 dereference failure: dead object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.5] line 1186 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.6] line 1186 dereference failure: invalid integer address in *ptr: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_obj_set_create_indexed_by_object_id
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_check_assignment
[__CPROVER_contracts_write_set_check_assignment.assertion.1] line 805 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.2] line 822 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.3] line 828 no offset bits overflow on CAR upper bound computation: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.unwind.1] line 837 unwinding assertion loop 0: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_record_deallocated
[__CPROVER_contracts_write_set_record_deallocated.unwind.1] line 740 unwinding assertion loop 0: SUCCESS

<builtin-library-free> function free
[free.frees.1] line 43 Check that ptr is freeable: SUCCESS

test.rs function _RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_
[_RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_.no_alloc_dealloc_in_ensures.1] line 3 Check that ensures do not allocate or deallocate memory: SUCCESS
[_RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_.no_alloc_dealloc_in_requires.1] line 3 Check that requires do not allocate or deallocate memory: SUCCESS
[_RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_.no_recursive_call.1] line 3 No recursive call to function _RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_ when checking contract _RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_: SUCCESS
[_RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_.single_top_level_call.1] line 3 Only a single top-level call to function _RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_ when checking contract _RNCNCNvCs8RDeLTht6ug_4test12modify_slices0_0s_0B5_: SUCCESS

test.rs function check_modify_slice
[check_modify_slice.precondition_instance.1] line 6 free argument must be NULL or valid pointer: SUCCESS
[check_modify_slice.precondition_instance.2] line 6 free argument must be dynamic object: SUCCESS
[check_modify_slice.precondition_instance.3] line 6 free argument has offset zero: SUCCESS
[check_modify_slice.precondition_instance.4] line 6 double free: SUCCESS
[check_modify_slice.precondition_instance.5] line 6 free called for new[] object: SUCCESS
[check_modify_slice.precondition_instance.6] line 6 free called for stack-allocated object: SUCCESS

test.rs function modify_slice::{closure#0}
[modify_slice::{closure#0}.unreachable.1] line 3 unreachable code: SUCCESS

test.rs function modify_slice::{closure#1}
[modify_slice::{closure#1}.unreachable.1] line 3 unreachable code: SUCCESS

test.rs function modify_slice::{closure#2}
[modify_slice::{closure#2}.assertion.1] line 3 |_| true: SUCCESS

test.rs function modify_slice::{closure#3}
[modify_slice::{closure#3}.unreachable.1] line 3 unreachable code: SUCCESS

Trace for std::slice::from_raw_parts::<'_, u32>.safety_check.1:

State 3 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[0]=255 (11111111)

State 4 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[1]=255 (11111111)

State 5 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[2]=255 (11111111)

State 6 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[3]=255 (11111111)

State 7 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[4]=255 (11111111)

State 8 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[5]=255 (11111111)

State 9 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[6]=255 (11111111)

State 10 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function __CPROVER_initialize line 48 thread 0
----------------------------------------------------
  test_6741b5a9f03e8776$$test$$global$$2$$.0[7]=255 (11111111)

State 33 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::of::<u32> line 48 thread 0
----------------------------------------------------
  var_0.0.case=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 34 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::of::<u32> line 49 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RINvMNtNtCs7WrvMewiLA2_4core3ptr9alignmentNtB3_9Alignment2ofmECs8RDeLTht6ug_4test.0.case=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 36 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new_in line 180 thread 0
----------------------------------------------------
  var_3.0.case=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 39 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new_in line 180 thread 0
----------------------------------------------------
  align.0.case=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 42 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 413 thread 0
----------------------------------------------------
  self.0.case=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 43 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::as_nonzero line 105 thread 0
----------------------------------------------------
  var_0.0.0=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 44 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::as_nonzero line 106 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMNtNtCs7WrvMewiLA2_4core3ptr9alignmentNtB2_9Alignment10as_nonzeroCs8RDeLTht6ug_4test.0.0=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 46 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 413 thread 0
----------------------------------------------------
  var_5.0.0=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 49 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 413 thread 0
----------------------------------------------------
  addr.0.0=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 52 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 96 thread 0
----------------------------------------------------
  self.0.0=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 53 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/nonzero.rs function std::num::NonZero::<usize>::get line 471 thread 0
----------------------------------------------------
  var_0=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 54 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/nonzero.rs function std::num::NonZero::<usize>::get line 472 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN4core3num7nonzero16NonZero$LT$T$GT$3get17hfc8aa78f7df86579E=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 56 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 96 thread 0
----------------------------------------------------
  var_3=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 59 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 96 thread 0
----------------------------------------------------
  addr=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 62 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance::<u8> line 600 thread 0
----------------------------------------------------
  addr=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 63 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance_mut::<u8> line 643 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 64 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance_mut::<u8> line 644 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RINvNtCs7WrvMewiLA2_4core3ptr22without_provenance_muthECs8RDeLTht6ug_4test=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 66 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance::<u8> line 600 thread 0
----------------------------------------------------
  var_2=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 67 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance::<u8> line 600 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 68 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance::<u8> line 601 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RINvNtCs7WrvMewiLA2_4core3ptr18without_provenancehECs8RDeLTht6ug_4test=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 70 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 96 thread 0
----------------------------------------------------
  pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 71 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 98 thread 0
----------------------------------------------------
  var_0.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 72 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 99 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN4core3ptr8non_null16NonNull$LT$T$GT$18without_provenance17h591a13a0a6a142d5E.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 74 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 413 thread 0
----------------------------------------------------
  var_4.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 77 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 413 thread 0
----------------------------------------------------
  pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 78 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::from_non_null line 106 thread 0
----------------------------------------------------
  var_0.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 79 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::from_non_null line 107 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN4core3ptr6unique15Unique$LT$T$GT$13from_non_null17ha9984406e50857bdE.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 81 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 413 thread 0
----------------------------------------------------
  ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 82 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 415 thread 0
----------------------------------------------------
  var_0.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 83 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::new_in line 416 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN5alloc7raw_vec20RawVecInner$LT$A$GT$6new_in17h7bdc0b3f43d670ceE.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 85 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new_in line 180 thread 0
----------------------------------------------------
  var_2.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 86 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new_in line 180 thread 0
----------------------------------------------------
  var_0.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 87 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new_in line 181 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMs0_NtCsi5dhE0JK53K_5alloc7raw_vecINtB5_6RawVecmE6new_inCs8RDeLTht6ug_4test.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 89 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new line 105 thread 0
----------------------------------------------------
  var_0.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 90 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::new line 106 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMNtCsi5dhE0JK53K_5alloc7raw_vecINtB2_6RawVecmE3newCs8RDeLTht6ug_4test.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 92 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::new line 435 thread 0
----------------------------------------------------
  var_1.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 93 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::new line 435 thread 0
----------------------------------------------------
  var_0.buf.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 94 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::new line 436 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMNtCsi5dhE0JK53K_5alloc3vecINtB2_3VecmE3newCs8RDeLTht6ug_4test.buf.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 96 file test.rs function check_modify_slice line 8 thread 0
----------------------------------------------------
  data.buf.inner.ptr.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 109 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32> line 512 thread 0
----------------------------------------------------
  var_3.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 112 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32> line 512 thread 0
----------------------------------------------------
  self.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 113 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::cast::<u32> line 155 thread 0
----------------------------------------------------
  var_3.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 116 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::cast::<u32> line 155 thread 0
----------------------------------------------------
  self.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 119 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::cast::<u32> line 488 thread 0
----------------------------------------------------
  self.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 120 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::as_ptr line 391 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 121 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::as_ptr line 392 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMs1_NtNtCs7WrvMewiLA2_4core3ptr8non_nullINtB5_7NonNullhE6as_ptrCs8RDeLTht6ug_4test=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 123 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::cast::<u32> line 488 thread 0
----------------------------------------------------
  var_4=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 124 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::cast::<u32> line 488 thread 0
----------------------------------------------------
  var_3=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 125 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::cast::<u32> line 488 thread 0
----------------------------------------------------
  var_2=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 126 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::cast::<u32> line 488 thread 0
----------------------------------------------------
  var_0.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 127 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::cast::<u32> line 489 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN4core3ptr8non_null16NonNull$LT$T$GT$4cast17h0de2b978b0986489E.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 129 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::cast::<u32> line 155 thread 0
----------------------------------------------------
  var_2.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 130 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::cast::<u32> line 155 thread 0
----------------------------------------------------
  var_0.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 131 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u8>::cast::<u32> line 156 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN4core3ptr6unique15Unique$LT$T$GT$4cast17h4c146549f42e8945E.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 133 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32> line 512 thread 0
----------------------------------------------------
  var_2.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 136 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32> line 512 thread 0
----------------------------------------------------
  self.pointer.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 137 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u32>::as_non_null_ptr line 120 thread 0
----------------------------------------------------
  var_0.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 138 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/unique.rs function std::ptr::Unique::<u32>::as_non_null_ptr line 121 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN4core3ptr6unique15Unique$LT$T$GT$15as_non_null_ptr17h99570721c767b141E.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 140 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32> line 512 thread 0
----------------------------------------------------
  var_0.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 141 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::non_null::<u32> line 513 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN5alloc7raw_vec20RawVecInner$LT$A$GT$8non_null17ha51ef3d7a52c0ae2E.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 143 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::ptr::<u32> line 507 thread 0
----------------------------------------------------
  var_2.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 146 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::ptr::<u32> line 507 thread 0
----------------------------------------------------
  self.pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 147 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u32>::as_ptr line 391 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 148 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u32>::as_ptr line 392 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMs1_NtNtCs7WrvMewiLA2_4core3ptr8non_nullINtB5_7NonNullmE6as_ptrCs8RDeLTht6ug_4test=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 150 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::ptr::<u32> line 507 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 151 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVecInner::ptr::<u32> line 508 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN5alloc7raw_vec20RawVecInner$LT$A$GT$3ptr17hcae6c6b409d5421bE=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 153 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::ptr line 286 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 154 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs function alloc::raw_vec::RawVec::<u32>::ptr line 287 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_ZN5alloc7raw_vec19RawVec$LT$T$C$A$GT$3ptr17h1f1b9aa4b183d7daE=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 156 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::as_ptr line 1696 thread 0
----------------------------------------------------
  var_2=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 157 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::as_ptr line 1696 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 158 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::as_ptr line 1697 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RNvMs_NtCsi5dhE0JK53K_5alloc3vecINtB4_3VecmE6as_ptrCs8RDeLTht6ug_4test=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 160 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::as_slice line 1600 thread 0
----------------------------------------------------
  var_2=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 163 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs function std::vec::Vec::<u32>::as_slice line 1600 thread 0
----------------------------------------------------
  data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 171 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs function std::slice::from_raw_parts::<'_, u32> line 138 thread 0
----------------------------------------------------
  data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 174 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::slice_from_raw_parts::<u32> line 886 thread 0
----------------------------------------------------
  data_pointer=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 175 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs function std::ptr::from_raw_parts::<[u32], u32> line 116 thread 0
----------------------------------------------------
  var_0.data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 176 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs function std::ptr::from_raw_parts::<[u32], u32> line 117 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RINvNtNtCs7WrvMewiLA2_4core3ptr8metadata14from_raw_partsSmmECs8RDeLTht6ug_4test.data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 178 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::slice_from_raw_parts::<u32> line 886 thread 0
----------------------------------------------------
  var_0.data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 179 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::slice_from_raw_parts::<u32> line 887 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RINvNtCs7WrvMewiLA2_4core3ptr20slice_from_raw_partsmECs8RDeLTht6ug_4test.data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 181 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs function std::slice::from_raw_parts::<'_, u32> line 138 thread 0
----------------------------------------------------
  var_8.data=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

Violated property:
  file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs function std::slice::from_raw_parts::<'_, u32> line 138 thread 0
  misaligned pointer to reference cast: address must be a multiple of its type's alignment
  (unsigned long int)var_8.data % 4 == 0



** 1 of 119 failed (2 iterations)
VERIFICATION FAILED
Manual Harness Summary:
Verification failed for - check_modify_slice
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

[zhassan-aws]

This tarball contains the goto binaries:

test.tar.gz

[zhassan-aws]

The instrumentation for the failing check is done here:

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

Line 372 in 6acad2f

let align_check = self.codegen_assert_assume(align_ok, PropertyClass::SafetyCheck,

[remi-delmas-3000]

First thing that jumps out in the counter example trace is the sheer lot of INVALID pointers leading up to the error.

At some point in the trace we see an address is cast to a pointer and yields an invalid pointer, this invalid pointer gets propagated all the way down the trace and triggers the assertion

State 59 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs function std::ptr::NonNull::<u8>::without_provenance line 96 thread 0
----------------------------------------------------
  addr=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 62 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance::<u8> line 600 thread 0
----------------------------------------------------
  addr=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 63 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs function std::ptr::without_provenance_mut::<u8> line 643 thread 0
----------------------------------------------------
  var_0=INVALID-65535 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

Using --stack-trace instead of --trace:

Trace for std::slice::from_raw_parts::<'_, u32>.safety_check.1:
  assertion failure file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/raw.rs line 138 column 9 function std::slice::from_raw_parts::<'_, u32>
  _RINvNtNtCs7WrvMewiLA2_4core5slice3raw14from_raw_partsmECs8RDeLTht6ug_4test((unsigned int *)(_ZN4kani8internal14init_contracts17h32078c4006d297a4E + 2), 0ul, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs line 1600 column 18 function std::vec::Vec::<u32>::as_slice
  _RNvMs_NtCsi5dhE0JK53K_5alloc3vecINtB4_3VecmE8as_sliceCs8RDeLTht6ug_4test(&data!0@1, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs line 3299 column 9 function <std::vec::Vec<u32> as std::ops::Deref>::deref
  _RNvXs6_NtCsi5dhE0JK53K_5alloc3vecINtB5_3VecmENtNtNtCs7WrvMewiLA2_4core3ops5deref5Deref5derefCs8RDeLTht6ug_4test(&data!0@1, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file test.rs line 9 column 25 function check_modify_slice
  _RNvCs8RDeLTht6ug_4test18check_modify_slice() file test.rs line 7 column 1 function check_modify_slice

[remi-delmas-3000]

Since the error happens even before entering modify_slice I suspect something's strange is going on kani::internal::init_contracts() (the invocation of that function would be the only thing that differs between a contract run and an non-contract run). Do we know what kani::internal::init_contracts is doing ? I can't find it in the GOTO binary.

there's a reference _ZN4kani8internal14init_contracts17h32078c4006d297a4E but no implementation.

[tautschnig]

The change that seems to make all the difference for us is the combination of rust-lang/rust@78e9621390 and rust-lang/rust@aadfd810f6: using Alignment::of will mean we invoke Alignment::new and apparently we don't manage to figure out that we can get away without creating a non-deterministic object.

[tautschnig]

Looking at the GOTO program (one could equally look at the MIR) it turns out Alignment::of never actually invokes Alignment::new and instead refers to a global static variable. That one, however, we've initialised to a non-deterministic value as part of our contracts instrumentation process.

Kani needs to mark global enums like enum AlignmentEnum as exempt from non-det initialisation by setting CNoNondetInitialization.

[remi-delmas-3000]

Confirmed by looking at the trace, std::ptr::Alignment::of::<u32> returns 18446744073709551615ul

State 34 file /home/ubuntu/.rustup/toolchains/nightly-2025-04-14-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs function std::ptr::Alignment::of::<u32> line 49 thread 0
----------------------------------------------------
  goto_symex$$return_value$$_RINvMNtNtCs7WrvMewiLA2_4core3ptr9alignmentNtB3_9Alignment2ofmECs8RDeLTht6ug_4test.0.case=18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)