Bug 8886 - Undefined behaviour in _wordcopy_fwd_aligned
Summary: Undefined behaviour in _wordcopy_fwd_aligned
Status: NEW
Alias: None
Product: uClibc
Classification: Unclassified
Component: Other (show other bugs)
Version: 0.9.34
Hardware: All All
: P5 normal
Target Milestone: ---
Assignee: unassigned
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2016-04-25 08:04 UTC by Michael Tautschnig
Modified: 2016-04-25 08:04 UTC (History)
1 user (show)

See Also:
Host:
Target:
Build:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Michael Tautschnig 2016-04-25 08:04:06 UTC
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