Precondition in memcpy is too strict

[danielsn]

In memcpy there is the following precondition:

 __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
                         __CPROVER_POINTER_OBJECT(src),
                         "memcpy src/dst overlap");

However, it is valid to memcpy between two segments of the same allocation, as long as the two segments themselves do not overlap. A better check would be something like

 __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
                         __CPROVER_POINTER_OBJECT(src) || (src > dst + n) || ( dst > src + n) ,
                         "memcpy src/dst overlap");

[kroening]

Indeed, thank you!