ID0001415: **This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001415 | Frama-C | Plug-in > Eva | public | 2013-05-03 | 2014-03-13 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 | ### Description : There was a bit of a discussion over an analysis made on an example provided by a StackOverflow user: http://stackoverflow.com/a/16356519/139746 The current message is: .../libc/string.h:54:[value] Function memcpy: precondition got status invalid. That is a bit frustrating. The localization of the call to memcpy() can be found just above in the log: [value] computing for function memcpy <- main. Called from mem.c:13. but the exact nature of the detected issue is only printed as a reference to libc/string.h, a file that the user did not even provide emself. There are at least two solutions suggested by the discussion: - annotate the libc preconditions with nice labels, and when a pre-condition fails, print any label it may have, or - print the entire ACSL pre-condition that failed, including any label it may have.