Limit dereferencing of __CPROVER_bitvector to objects with size multiple of 8

[NlightNFotis]

This should be resolving the first issue reported in #7104 by limiting the derefencing/taking of address of bit vector objects whose size is less than 8.

This is for now a draft, as I continue to QA the changes in this PR.

This is a partial solution to the problem described in #7104. There's going to be another PR with the solution to the second issue described there.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[NlightNFotis]

Hi @tautschnig,

this PR is now making bit vector dereferences that are not size-multiple of 8 fail type checking.

This had the side-effect of causing some tests you added recently to fail, for instance:

__CPROVER_bitvector[1] *bptr = &A[len - 1];
*bptr = 0;

This construct in regression/cbmc/byte_update16/main.c is now illegal.

Is this the way to go, or should we be doing things a different way? If yes, shall we delete the tests (given that they appear to have been invalidated by this change).

[tautschnig]

I'm not sure the C front-end is a sufficiently general layer for this check: we might need to do it during goto-program conversion, or perhaps even later (maybe even the back-end)? I don't think it's a C-specific issue at all.

[tautschnig]

This construct in regression/cbmc/byte_update16/main.c is now illegal.

Is this the way to go, or should we be doing things a different way? If yes, shall we delete the tests (given that they appear to have been invalidated by this change).

Knowing that this is a non-trivial request: I don't think this test should be removed without replacement. It's right that this shouldn't be done via the C front-end, and not be done via pointers. What this test is supposed to exercise, however, could safely be exercised via the (existing, to-be extended) unit test of byte-operator lowering. So the gist of this regression test (which can most easily be found by running this test through cbmc --program-only) should be turned into a couple of expressions to be added to that unit test (and be subjected to lowering).

[NlightNFotis]

The problem this PR is supposed to fix was fixed in #7444.

This is now no longer relevant as a PR, so closing it now.