Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001415Frama-CPlug-in > value analysispublic2013-05-03 14:422014-03-13 15:57
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0003930)
yakobowski (manager)
2013-05-30 23:10
edited on: 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)
2014-02-12 16:58

Fix committed to stable/neon branch.

- 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 Checkin
2013-06-11 22:31 svn Status assigned => resolved
2013-06-11 22:31 svn Resolution open => fixed
2013-06-26 16:11 svn Checkin
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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker