A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/model-checking/kani/issues/357 below:

Unimplemented `head:tail` pattern for slices. · Issue #357 · model-checking/kani · GitHub

I tried this code:

fn main() {
    let slice = &[1, 2, 3][..];
    if let [head, tail @ ..] = slice {
        assert!(head == &slice[0]);
        assert!(tail == &slice[1..]);
    } else {
        unreachable!();
    }
}

using the following command line invocation:

with RMC version: 6962a67

I expected to see this happen: verification succeeds.

Instead, this happened: RMC panics with the following error:

thread 'rustc' panicked at 'not implemented', compiler/rustc_codegen_llvm/src/gotoc/place.rs:352:48
stack backtrace:
   0: rust_begin_unwind
             at ./library/std/src/panicking.rs:515:5
   1: core::panicking::panic_fmt
             at ./library/core/src/panicking.rs:92:14
   2: core::panicking::panic
             at ./library/core/src/panicking.rs:50:5
   3: rustc_codegen_llvm::gotoc::place::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_projection
             at ./compiler/rustc_codegen_llvm/src/gotoc/place.rs:352:48
   4: rustc_codegen_llvm::gotoc::place::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_place::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/place.rs:400:53
   5: core::iter::adapters::copied::copy_fold::{{closure}}
             at ./library/core/src/iter/adapters/copied.rs:26:22
   6: core::iter::traits::iterator::Iterator::fold
             at ./library/core/src/iter/traits/iterator.rs:2173:21
   7: <core::iter::adapters::copied::Copied<I> as core::iter::traits::iterator::Iterator>::fold
             at ./library/core/src/iter/adapters/copied.rs:62:9
   8: rustc_codegen_llvm::gotoc::place::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_place
             at ./compiler/rustc_codegen_llvm/src/gotoc/place.rs:398:9
   9: rustc_codegen_llvm::gotoc::rvalue::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_rvalue_ref
             at ./compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs:105:26
  10: rustc_codegen_llvm::gotoc::rvalue::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_rvalue
             at ./compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs:386:63
  11: rustc_codegen_llvm::gotoc::statement::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_statement
             at ./compiler/rustc_codegen_llvm/src/gotoc/statement.rs:462:60
  12: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_block
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:124:32
  13: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_function::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:207:71
  14: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at ./library/core/src/iter/traits/iterator.rs:733:29
  15: core::iter::adapters::map::map_fold::{{closure}}
             at ./library/core/src/iter/adapters/map.rs:82:21
  16: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold::enumerate::{{closure}}
             at ./library/core/src/iter/adapters/enumerate.rs:104:27
  17: core::iter::traits::iterator::Iterator::fold
             at ./library/core/src/iter/traits/iterator.rs:2173:21
  18: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold
             at ./library/core/src/iter/adapters/enumerate.rs:110:9
  19: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at ./library/core/src/iter/adapters/map.rs:122:9
  20: core::iter::traits::iterator::Iterator::for_each
             at ./library/core/src/iter/traits/iterator.rs:736:9
  21: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_function
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:207:13
  22: <rustc_codegen_llvm::gotoc::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:393:35
  23: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::call_with_panic_debug_info::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:103:13
  24: std::thread::local::LocalKey<T>::try_with
             at ./library/std/src/thread/local.rs:399:16
  25: std::thread::local::LocalKey<T>::with
             at ./library/std/src/thread/local.rs:375:9
  26: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::call_with_panic_debug_info
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:101:9
  27: <rustc_codegen_llvm::gotoc::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:392:25
  28: rustc_interface::passes::start_codegen::{{closure}}
             at ./compiler/rustc_interface/src/passes.rs:1054:9
  29: rustc_data_structures::profiling::VerboseTimingGuard::run
             at ./compiler/rustc_data_structures/src/profiling.rs:573:9
  30: rustc_session::utils::<impl rustc_session::session::Session>::time
             at ./compiler/rustc_session/src/utils.rs:16:9
  31: rustc_interface::passes::start_codegen
             at ./compiler/rustc_interface/src/passes.rs:1053:19
  32: rustc_interface::queries::Queries::ongoing_codegen::{{closure}}::{{closure}}
             at ./compiler/rustc_interface/src/queries.rs:254:20
  33: rustc_interface::passes::QueryContext::enter::{{closure}}
             at ./compiler/rustc_interface/src/passes.rs:780:42
  34: rustc_middle::ty::context::tls::enter_context::{{closure}}
             at ./compiler/rustc_middle/src/ty/context.rs:1744:50
  35: rustc_middle::ty::context::tls::set_tlv
             at ./compiler/rustc_middle/src/ty/context.rs:1728:9
  36: rustc_middle::ty::context::tls::enter_context
             at ./compiler/rustc_middle/src/ty/context.rs:1744:9
  37: rustc_interface::passes::QueryContext::enter
             at ./compiler/rustc_interface/src/passes.rs:780:9
  38: rustc_interface::queries::Queries::ongoing_codegen::{{closure}}
             at ./compiler/rustc_interface/src/queries.rs:245:13
  39: rustc_interface::queries::Query<T>::compute
             at ./compiler/rustc_interface/src/queries.rs:38:28
  40: rustc_interface::queries::Queries::ongoing_codegen
             at ./compiler/rustc_interface/src/queries.rs:243:9
  41: rustc_driver::run_compiler::{{closure}}::{{closure}}
             at ./compiler/rustc_driver/src/lib.rs:407:13
  42: rustc_interface::queries::<impl rustc_interface::interface::Compiler>::enter
             at ./compiler/rustc_interface/src/queries.rs:394:19
  43: rustc_driver::run_compiler::{{closure}}
             at ./compiler/rustc_driver/src/lib.rs:312:22
  44: rustc_interface::interface::create_compiler_and_run::{{closure}}
             at ./compiler/rustc_interface/src/interface.rs:208:13
  45: rustc_span::with_source_map
             at ./compiler/rustc_span/src/lib.rs:911:5
  46: rustc_interface::interface::create_compiler_and_run
             at ./compiler/rustc_interface/src/interface.rs:202:5
  47: rustc_interface::interface::run_compiler::{{closure}}
             at ./compiler/rustc_interface/src/interface.rs:224:12
  48: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::{{closure}}::{{closure}}
             at ./compiler/rustc_interface/src/util.rs:155:13
  49: scoped_tls::ScopedKey<T>::set
             at /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/scoped-tls-1.0.0/src/lib.rs:137:9
  50: rustc_span::create_session_globals_then
             at ./compiler/rustc_span/src/lib.rs:105:5
  51: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::{{closure}}
             at ./compiler/rustc_interface/src/util.rs:153:9
  52: rustc_interface::util::scoped_thread::{{closure}}
             at ./compiler/rustc_interface/src/util.rs:128:24

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4