Feature request: supported unsized globals

[N1ark]

Title is misleading, but we need to support globals that may be unsized (whether that means having unsized globals, or having sized globals that can be referenced with metadata, i don't know). This is e.g. an issue for c"strings", where the translation creates unsized variables in the store (notice the _2; Cstr is defined as core::ffi::c_str::CStr { inner: [i8] }

charon/charon/tests/ui/multi-target/cstr.out

Lines 11 to 22 in 985e04c

	fn test_crate::main::x86_64-unknown-linux-gnu()
	{
	let _0: (); // return
	let _1: &'1 core::ffi::c_str::CStr::x86_64-unknown-linux-gnu; // anonymous local
	let _2: core::ffi::c_str::CStr::x86_64-unknown-linux-gnu; // anonymous local
	let _3: &'2 core::ffi::c_str::CStr::x86_64-unknown-linux-gnu; // anonymous local
	_0 = ()
	storage_live(_1)
	storage_live(_2)
	_2 = core::ffi::c_str::CStr::x86_64-unknown-linux-gnu { inner: const [49i8, 50i8, 51i8, 0i8] }
	storage_live(_3)

I'm not aware of other cases where this may happen, but I haven't tried much; maybe a const FOO: &dyn Trait or something like that? Possibly related: #1225

[Nadrieril]

Oh that's a fun example. You should only be able to construct an unsized value by transmuting/unsizing pointers. I suspect constant unevaluation might be the culprit for inventing an unsized local like that...