You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
// run-passstructFat<T: ?Sized>{f1:isize,f2:&'static str,ptr:T}// x is a fat pointerfnfoo(x:&Fat<[isize]>){let y = &x.ptr;assert_eq!(y[0], 1);}#[kani::proof]pubfnmain(){// With a vec of ints.let f1 = Fat{f1:5,f2:"some str",ptr:[1,2,3]};foo(&f1);}
using the following command line invocation:
RUSTFLAGS="-Zmir-opt-level=2" kani dst-struct.rs
with Kani version: 0.34.0
I expected to see this happen: explanation
Instead, this happened: explanation
Kani Rust Verifier 0.34.0 (standalone)
warning: fields `f1` and `f2` are never read
--> dst-struct.rs:3:5
|
2 | struct Fat<T: ?Sized> {
| --- fields in this struct
3 | f1: isize,
| ^^
4 | f2: &'static str,
| ^^
|
= note: `#[warn(dead_code)]` on by default
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:1029:9:
BinaryOperation Expression does not typecheck Plus Expr { value: Member { lhs: Expr { value: Dereference(Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_RNvCs1amkcWqkymA_10dst_struct3foo::1::var_1::x" }, typ: StructTag("tag-&_212445076144030373480958249808482652875"), location: None, size_of_annotation: None }, field: "data" }, typ: Pointer { typ: StructTag("tag-_212445076144030373480958249808482652875") }, location: None, size_of_annotation: None }), typ: StructTag("tag-_212445076144030373480958249808482652875"), location: None, size_of_annotation: None }, field: "ptr" }, typ: FlexibleArray { typ: CInteger(SSizeT) }, location: None, size_of_annotation: None } Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None, size_of_annotation: None }
stack backtrace:
0: 0x7fba0016319c - std::backtrace_rs::backtrace::libunwind::trace::haf256adafafbe58d
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
1: 0x7fba0016319c - std::backtrace_rs::backtrace::trace_unsynchronized::hfe1951132ff691c0
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x7fba0016319c - std::sys_common::backtrace::_print_fmt::h9a0fe52434930c36
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:67:5
3: 0x7fba0016319c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h24adccbf3e1ada83
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:44:22
4: 0x7fba001c989c - core::fmt::rt::Argument::fmt::h18ba555e398addfe
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/fmt/rt.rs:138:9
5: 0x7fba001c989c - core::fmt::write::hbf3ee2d80be74759
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/fmt/mod.rs:1094:21
6: 0x7fba0015590e - std::io::Write::write_fmt::hfc2b3251522ff943
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/io/mod.rs:1714:15
7: 0x7fba00162f85 - std::sys_common::backtrace::_print::hfdc8ddb5f3ddee36
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:47:5
8: 0x7fba00162f85 - std::sys_common::backtrace::print::h316f264b298c7a30
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:34:9
9: 0x7fba001660da - std::panicking::panic_hook_with_disk_dump::{{closure}}::h136bbb963feeea4a
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:278:22
10: 0x7fba00165d73 - std::panicking::panic_hook_with_disk_dump::hd91a018a982a84f7
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:312:9
11: 0x55afc674771d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::hbdcd1e2153d1f24b
12: 0x55afc6745e63 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hc68eaec26ff64861
13: 0x7fba00166980 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hd99b1fe24ccd07b5
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2021:9
14: 0x7fba00166980 - std::panicking::rust_panic_with_hook::h1593161995c9c003
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:733:13
15: 0x7fba00166707 - std::panicking::begin_panic_handler::{{closure}}::h6b4a934e37237346
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:621:13
16: 0x7fba001636d6 - std::sys_common::backtrace::__rust_end_short_backtrace::h365e31c6291fdffa
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:170:18
17: 0x7fba00166452 - rust_begin_unwind
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:617:5
18: 0x7fba001c5c53 - core::panicking::panic_fmt::hbd2564497e278309
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/panicking.rs:67:14
19: 0x55afc6962373 - cprover_bindings::goto_program::expr::Expr::binop::hfde2f1595b998cec
20: 0x55afc6962a42 - cprover_bindings::goto_program::expr::Expr::plus::h7e1518fc405778fe
21: 0x55afc66e82ff - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection::h8ef94609a9faa773
22: 0x55afc66ea182 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::hca2771dc57ddaeac
23: 0x55afc66dee82 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::hdb64779d690c624d
24: 0x55afc66ec853 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h2d1feaaf678662c2
25: 0x55afc66f9f93 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::hbe3635206b55fa31
26: 0x55afc66b2860 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::had8f57135e8154af
27: 0x55afc670f87b - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::he08100d10d5a8739
28: 0x55afc67dbf7e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h1c7461510b84019a
29: 0x55afc67e09e5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h72f45c460ba9f3e3
30: 0x7fba02694dc2 - <rustc_session[83a530cc07544870]::session::Session>::time::<alloc[b2a4fa84f81d55c8]::boxed::Box<dyn core[8e2a8f22f3da315]::any::Any>, rustc_interface[b10bd5cb1b971de9]::passes::start_codegen::{closure#0}>
31: 0x7fba0269490b - rustc_interface[b10bd5cb1b971de9]::passes::start_codegen
32: 0x7fba0268ef1a - <rustc_middle[32728bc096d751c7]::ty::context::GlobalCtxt>::enter::<<rustc_interface[b10bd5cb1b971de9]::queries::Queries>::ongoing_codegen::{closure#0}, core[8e2a8f22f3da315]::result::Result<alloc[b2a4fa84f81d55c8]::boxed::Box<dyn core[8e2a8f22f3da315]::any::Any>, rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
33: 0x7fba0268df53 - <rustc_interface[b10bd5cb1b971de9]::interface::Compiler>::enter::<rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}::{closure#2}, core[8e2a8f22f3da315]::result::Result<core[8e2a8f22f3da315]::option::Option<rustc_interface[b10bd5cb1b971de9]::queries::Linker>, rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
34: 0x7fba02686fc8 - std[b7e5a9c79ea9fbed]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[b10bd5cb1b971de9]::util::run_in_thread_pool_with_globals<rustc_interface[b10bd5cb1b971de9]::interface::run_compiler<core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>, rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}>::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
35: 0x7fba0268674e - <<std[b7e5a9c79ea9fbed]::thread::Builder>::spawn_unchecked_<rustc_interface[b10bd5cb1b971de9]::util::run_in_thread_pool_with_globals<rustc_interface[b10bd5cb1b971de9]::interface::run_compiler<core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>, rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}>::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#1} as core[8e2a8f22f3da315]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
36: 0x7fba00171125 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hb18992c0c074fb04
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2007:9
37: 0x7fba00171125 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::ha4998f5f9033c44e
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2007:9
38: 0x7fba00171125 - std::sys::unix::thread::Thread::new::thread_start::h3370231efa79af31
at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys/unix/thread.rs:108:17
39: 0x7fb9ffc8c9eb - <unknown>
40: 0x7fb9ffd10ebc - <unknown>
41: 0x0 - <unknown>
Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md
[Kani] current codegen item: codegen_function: foo
_RNvCs1amkcWqkymA_10dst_struct3foo
[Kani] current codegen location: Loc { file: "/tmp/kani/dst-struct.rs", function: None, start_line: 9, start_col: Some(1), end_line: 9, end_col: Some(25) }
warning: 1 warning emitted
error: /home/matthias/.kani/kani-0.34.0/bin/kani-compiler exited with status exit status: 101
The text was updated successfully, but these errors were encountered:
I tried this code:
rust/tests/ui/dynamically-sized-types/dst-struct.rs
using the following command line invocation:
with Kani version: 0.34.0
I expected to see this happen: explanation
Instead, this happened: explanation
The text was updated successfully, but these errors were encountered: