Missing functions produce non-informative property descriptions

[adpaco-aws]

Upgrading the CBMC version to 5.59.0 caused regression failures related to missing functions. These are now failing with the description "assertion", apparently because they do not include source locations.

[adpaco-aws]

According to @tautschnig , this is due to https://github.com/diffblue/cbmc/pull/6902 but the intended behavior was to get the following message instead:

	 - Status: FAILURE
	 - Description: "undefined function should be unreachable"

This is what should be expected when we upgrade to the next version of CBMC. In the meantime, I've submitted changes to the expected results according to the current output in #1270

[tautschnig]

I believe the problem is that the symbols you create for missing functions do not have a source location. Looking at _ZN60_$LT$alloc..string..String$u20$as$u20$core..clone..Clone$GT$5clone17hd1d44edec193123bE as is generated from the following piece of code (due to @jaisnan):

#[kani::proof]
fn main() {
    let x = String::from("foo");
    let y = x.clone();
    assert_eq!("foo", y);
}

I see that the source location is nil, which is unexpected. The CBMC code base would expect that there at least be a source location associated with the declaration, even when the definition is unavailable. This might be a C legacy, but in Kani you'd have a source location.

[adpaco-aws]

Fix was done in #1513 but didn't close this issue automatically.