| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0001648 | Frama-C | Kernel | public | 2014-02-17 17:21 | 2018-11-30 11:36 | ||||||||
| Reporter | pascal | ||||||||||||
| Assigned To | maroneze | ||||||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | |||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0001648: Wrong specification for standard library function memmove | ||||||||||||
| Description | 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. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
| There are no notes attached to this issue. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2014-02-17 17:21 | pascal | New Issue | |
| 2014-03-15 10:55 | signoles | Assigned To | => Matthieu Lemerre |
| 2014-03-15 10:55 | signoles | Status | new => assigned |
| 2018-11-30 11:36 | signoles | Assigned To | Matthieu Lemerre => maroneze |
| Issue History |