Bug 8886

Running CBMC (C bounded model checker) on code that uses uClibc, it reports a genuine counterexample proving the possibility of memory errors as follows:

For

static void _wordcopy_fwd_aligned (long int dstp, long int srcp, size_t len)

and len < 5, the subtractions performed in the switch/case statement yield pointers outside the object pointed to. This is undefined behaviour as described in C standard section 6.5.6, paragraph 8.

It seems the assembly-level implementation does not use such an approach, and therefore is safe.

Best,
Michael