"unions are not supported"

[djc]

I finally followed up with the instructions in #1193 (comment) and tried to run Prusti on rustls. However, after some time it failed:

[2023-02-26T20:39:14Z INFO  prusti_viper::encoder::encoder] Encoding: rustls::msgs::persist::ClientSessionValue::common (rustls::msgs::persist::{impl#0}::common)
thread 'rustc' panicked at 'called `Result::unwrap()` on an `Err` value: Spanned(SpannedEncodingError { error: Unsupported("unions are not supported"), span: MultiSpan { primary_spans: [/Users/djc/.cargo/registry/src/github.com-1ecc6299db9ec823/ring-0.16.20/src/digest.rs:439:1: 439:12 (#0)], span_labels: [] }, help: None, notes: [] })', prusti-viper/src/encoder/encoder.rs:401:23
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::result::unwrap_failed
   3: prusti_viper::encoder::encoder::Encoder::encode_discriminant_func_app
   4: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_assign
   5: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement_at
   6: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_blocks_group
   7: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
   8: prusti_viper::encoder::encoder::Encoder::encode_procedure
   9: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
  10: prusti_viper::verifier::Verifier::verify
  11: rustc_interface::queries::QueryResult<rustc_interface::passes::QueryContext>::enter
  12: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis
  13: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
  14: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  15: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Which is here:

#[derive(Clone, Copy)] // XXX: Why do we need to be `Copy`?
#[repr(C)]
union State {
    as64: [Wrapping<u64>; sha2::CHAINING_WORDS],
    as32: [Wrapping<u32>; sha2::CHAINING_WORDS],
}

#[derive(Clone, Copy)]
#[repr(C)]
union Output {
    as64: [BigEndian<u64>; 512 / 8 / core::mem::size_of::<BigEndian<u64>>()],
    as32: [BigEndian<u32>; 256 / 8 / core::mem::size_of::<BigEndian<u32>>()],
}

So not sure how that fits in your development goals/roadmap, just showing that there is some real world code out there using unions (a quick search in the existing issues didn't turn up an existing issue).