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