2021-02-24 19:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001415Frama-CPlug-in > Evapublic2014-03-13 15:57
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001415: Logging just enough information for failed pre-conditions
DescriptionThere 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0003930

yakobowski (manager)

Last edited: 2013-05-31 21:44

Properties line numbers will be shown together with the property name. This also require updating the libc to be useful, though.

~0004570

yakobowski (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-05-03 14:42 pascal New Issue
2013-05-03 14:42 pascal Status new => assigned
2013-05-03 14:42 pascal Assigned To => yakobowski
2013-05-30 23:10 yakobowski Note Added: 0003930
2013-05-30 23:11 yakobowski Note Edited: 0003930
2013-05-31 21:44 yakobowski Note Edited: 0003930
2013-06-11 22:31 svn
2013-06-11 22:31 svn Status assigned => resolved
2013-06-11 22:31 svn Resolution open => fixed
2013-06-26 16:11 svn
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master c834f826
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 9006781c
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon c834f826
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon 9006781c
2014-02-12 16:58 yakobowski Note Added: 0004570
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History