0001415: Logging just enough information for failed pre-conditions

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001415

Frama-C

Plug-in > value analysis

public

2013-05-03 14:42

2014-03-13 15:57

Reporter

pascal

Assigned To

yakobowski

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001415: Logging just enough information for failed pre-conditions

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.

Tags

No 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