Logging just enough information for failed pre-conditions
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.