Shadow memory does not currently work on big-endian architectures

[tautschnig]

Running cbmc --big-endian regression/cbmc-shadow-memory/float1/main.c yields VERIFICATION FAILED (and so do several other tests in the cbmc-shadow-memory suite). As far as I can tell, the problem is that compute_max_over_bytes uses byte extract with a value type that isn't even a full byte (it might just be 7 bits). This code should either extract bits (with suitable offset), or extract full bytes and then apply a mask (adjusted for endianness).

CBMC version: cbmc-5.95.1 or later
Operating system: Any big-endian platform, or running cbmc with --big-endian
Exact command line resulting in the issue: See above
What behaviour did you expect: Verification results are independent of endianness.
What happened instead: See above