Fix ICE on non-literal cover/assert/check message expressions

[ivmat]

Problem

kani-compiler's codegen hooks for kani::cover, kani::assert, kani::check and the internal
safety-check/unsupported-check hooks all call gcx.extract_const_message(&msg).unwrap() to recover the
message string.

extract_const_message returns None whenever the message operand does not codegen down to a
string-literal constant — for example when it is a function parameter — so the .unwrap() produces an
internal compiler error rather than a normal diagnostic.

Reproducer (kani::cover case):

#[kani::proof]
fn main() {
    let msg = "not a literal";
    kani::cover!(true, msg);
}

This still reproduces on main: all six extract_const_message(&msg).unwrap() call sites are present
in kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs.

Fix

Add extract_msg_or_err, which mirrors the existing utils::span_err + abort_if_errors pattern
already used by neighbouring intrinsic codegen in the same file, and use it at all six call sites
(Cover, Assert, UnsupportedCheck, SafetyCheck, SafetyCheckNoAssume, Check).

Each now emits a spanned `<construct>` message must be a string literal error and aborts
compilation cleanly instead of panicking.

Tests

UI regression tests modelled on the existing tests/ui/ice-size-overflow test (a prior
"ICE → clean error" regression test):

• tests/ui/cover-non-literal-message/
• tests/ui/assert-non-literal-message/

kani::check is pub(crate) in library/kani_core/src/lib.rs with no public re-export, so user code
cannot invoke it directly (it fails earlier with E0425). The remaining hooks
(safety_check, safety_check_no_assume, unsupported_check) are compiler-generated and not
reachable from user code either, so neither is given a UI test.

Testing performed, and what was not run

• cargo build -p kani-compiler on this branch — passes.
• The two UI tests were verified by direct invocation against a locally built driver/compiler,
  comparing output against expected the same way compiletest's verify_output does.

Stated plainly rather than left to be assumed:

• compiletest itself was not run. It invokes a binary named kani resolved through PATH, which
  in a source checkout is the kani-verifier proxy resolving ${KANI_HOME}, not the local build.
  Wiring that up would have meant installing over the machine's global Kani install.
• clippy was not run — it is not installed for the pinned nightly toolchain, and installing it
  would have mutated the pin.

Happy to adjust the diagnostic wording or the test placement if you'd prefer something different.