Treat pointer and Box locals of function items as ordinary variables

[srivatsansamraj]

codegen_local_fndef replaced a local whose type is a raw pointer to a function item, or a Box of one, with a fixed expression: &f::FnDefSingleton, or a Box literal around it. That is only right for the function item itself, which is zero-sized, so all its values are the same. A pointer holds whatever was assigned to it. The substitution caused three failures:

• ICE: Function should've been declared before usage, was: Can't take address of Expr #2255: building &f::FnDefSingleton needs f's symbol, which reachability does not declare when f is only pointed to ({:p} of &foo), so codegen panics at operand.rs:697.
• CBMC symex fails on a function item called through Box<dyn Fn>: l2_rename_rvalues case address_of not handled #4857 and Kani fails with l2_rename_values case struct' not handled` #1257: a write to such a local assigns to &f::FnDefSingleton or to a struct literal, neither of which is an lvalue, and CBMC stops with l2_rename_rvalues case `address_of' not handled.
• With Drop writes to locals that stand for a function item #4860, which drops those writes, reads still return the singleton, so a null *const F to a function item reads as non-null and an assertion that it is non-null verifies.

This keeps only the FnDef arm, so pointer and Box locals of function items are ordinary variables, and deletes box_value, whose only caller was the Box arm.

The new test FunctionSymbols/fn_item_address.rs covers the #2255 program, the value of a pointer to a function item, and a should_panic harness that fails if a null one reads as non-null. DynTrait/boxed_fn_item.rs drops --only-codegen and now verifies. The programs from #4857 and #1257 verify, and variants with a wrong expected value fail. Calls through Box<dyn Fn>, Box<dyn FnMut> and Box<dyn FnOnce> of a function item, and reads and calls through a dangling pointer to one, verify. The kani and expected suites pass, apart from two Quantifiers tests that fail the same way on main on this machine.

This replaces #4860.

Resolves #2255
Resolves #4857
Resolves #1257

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

[srivatsansamraj]

@CYJ904 @Tianshu-Huang @wodex1nhaoIeng @acearyanarun for review.

In Kani, a function item (foo used as a value) is zero-sized, so Kani stands one global object in for it. Kani did the same for a pointer to a function item and for a Box of one: instead of a real variable, it used a fixed "address of foo". A pointer can hold any address, including null, so that shortcut was wrong. It caused a crash when printing &foo with {:p} (#2255), a CBMC error when writing to such a pointer (#4857, #1257), and, with our earlier fix #4860, a wrong result: a null pointer read as non-null.

This PR removes the shortcut for pointers and boxes, so they are ordinary variables.