Drop writes to locals that stand for a function item

[srivatsansamraj]

Writes to a local whose type is a raw pointer to a function item, or a Box of one, are now dropped. Before, they became assignments CBMC cannot execute, and verification stopped with l2_rename_rvalues case `address_of' not handled.

codegen_local replaces such a local with a reference to the function item (codegen_local_fndef): &f::FnDefSingleton for the pointer, and a Box struct literal around it for the box. That is right for reads, since the value is the same everywhere. But the same place codegen builds the target of a write, so the program assigned to &f::FnDefSingleton or to the struct literal, and neither is an lvalue. A local of the function item type itself was already safe: it is zero-sized, and assignments to zero-sized types are skipped.

The new is_fndef_local is true for such a local. The Assign arm skips the write, as it does for zero-sized types, and codegen_expr_to_place_stable emits the call without a left side, as it does for (). Reads are unchanged, since they never used the local's variable.

The raw-pointer case fails on main without any Box:

fn call_through_raw<F: Fn(i32) -> i32>(f: F) -> i32 {
    let p: *const F = &f;
    unsafe { (*p)(1) }
}

A new test, FunctionCall/fn_item_raw_ptr.rs, writes such a pointer once by assignment and once from a call's return value. Both harnesses fail on main. With either half of the change reverted, that half's harness fails.

The Box case needs #4801 to get through codegen first. With #4801 and this change together, the program in #4857 and the one in #1257 both verify, and DynTrait/boxed_fn_item.rs can drop --only-codegen. I'll make that change in whichever of the two PRs merges second.

Resolves #4857

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[srivatsansamraj]

Converting to draft: dropping the writes leaves every read of the local returning the function's singleton, so a null *const F to a function item reads as non-null and assert!(!p.is_null()) on it verifies. We'll replace this with a change that stops substituting pointer and Box locals of function items, which also fixes #4857 and #2255.

[srivatsansamraj]

Closing in favour of #4892.