Analysing example with `memcpy` and using --no-simplify causes INVARIANT violation

[thomasspriggs]

Exact command line resulting in the issue: cbmc ./memcpy_simple1.c --no-simplify

memcpy_simple1.c

```C #include #include #include int main() { uint8_t vals_in[4] = {1, 2, 3, 4}; memcpy(vals_in + 2, vals_in, 2); assert(0); }; ```

What behaviour did you expect: Assertion failure for the assert(0);. What happened instead: INVARIANT violation

Details

``` cbmc ./memcpy_simple1.c --no-simplify CBMC version 5.91.0 (cbmc-5.91.0-42-g4173f7e86f) 64-bit x86_64 linux Parsing ./memcpy_simple1.c Converting Type-checking memcpy_simple1 Generating GOTO Program Adding CPROVER library (x86_64) Removal of function pointers and virtual functions Generic Property Instrumentation Running with 8 object bits, 56 offset bits (default) Starting Bounded Model Checking Runtime Symex: 0.00345228s size of program expression: 64 steps simple slicing removed 5 assignments Generated 4 VCC(s), 4 remaining after simplification Runtime Postprocess Equation: 1.3063e-05s Passing problem to propositional reduction converting SSA --- begin invariant violation report --- Invariant check failed File: cbmc/src/util/lower_byte_operators.cpp:2536 function: lower_byte_update Condition: update_bits.has_value() Reason: constant size-of should imply fixed bit width ```

[martin-cs]

I'm not exactly surprised by this. Having "things are in 'rewrite normal form'" is useful invariant and does simplify a bunch of things -- that's sort of the point of the simplifier, not just simplifying expressions but also the code that handles them. I guess we need to decide where the 'rewrite normal form' can be assumed and this should be enforced and tested. That may well mean we have to reconsider whether we want --no-simplify which is a very old debug flag. I feel like there are better ways of achieving assurance that the simplifier is working.