Frama-C Bug Tracking System - Frama-C
View Issue Details
0001648Frama-CKernelpublic2014-02-17 17:212018-11-30 11:36
pascal 
maroneze 
normalmajoralways
assignedopen 
 
 
0001648: Wrong specification for standard library function memmove
CONTEXT:
This issue does not originate from an industrial application. It is reported for the lulz.

DESCRIPTION:
The post-condition for memmove() incorrectly describes its effects when source and destination overlap.

/*@ ...
  @ ensures memcmp((char*)dest,(char*)src,n) == 0;
  ...
  @*/
extern void *memmove(void *dest, const void *src, size_t n);

In order to be maximally useful, the memcmp logic function, which is defined thus:

/*@ axiomatic MemCmp {
  @ logic ℤ memcmp{L}(char *s1, char *s2, ℤ n)
  @ reads s1[0..n - 1], s2[0..n - 1];
  ...

would need to be parameterized by two labels L1 and L2, and state that the memory zone pointed by s1 in L1 is identical to the memory zone pointed by s2 in L2.
No tags attached.
Issue History
2014-02-17 17:21pascalNew Issue
2014-03-15 10:55signolesAssigned To => Matthieu Lemerre
2014-03-15 10:55signolesStatusnew => assigned
2018-11-30 11:36signolesAssigned ToMatthieu Lemerre => maroneze

There are no notes attached to this issue.