MIR: Require users to initialize `Freeze` statics in specifications

[RyanGlScott]

(Spun out from #1941 (comment))

As of #1941, the MIR backend will initialize immutable statics before simulating a function, but it will not initialize mutable statics, instead requiring users to do so themselves. Currently, we determine this by simply checking if the static is marked mut or not, but this check is not as precise as it could be. Any type that implements the Freeze trait (e.g., AtomicU8) are compiled to mutable LLVM globals, and therefore, they can be modified at runtime. We should include Freeze-able types as part of the check.

[RyanGlScott]

We will also want to take Freeze-able types into account when determining the mutable allocations in the postconditions of an override.