- 
                Notifications
    You must be signed in to change notification settings 
- Fork 84
Closed
Description
Our old-style library function specifications for memmove are the following:
analyzer/src/analyses/libraryFunctions.ml
Lines 764 to 766 in 91388ef
| "memmove", writes [2;3];(*keep [2;3]*) | |
| "__builtin_memmove", writes [2;3];(*keep [2;3]*) | |
| "__builtin___memmove_chk", writes [2;3];(*keep [2;3]*) | 
These seem to be flipped, because the actual signature is
void* memmove( void* dest, const void* src, size_t count );So the first argument is written and the second one read.
This causes some spurious race warning in chrony (due to the extra src write) but also could be unsound (due to the missing dst write).
This could also be done in #1079.