Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001415Frama-CPlug-in > Evapublic2013-05-03 14:422014-03-13 15:57
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
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: 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
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.
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
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker