Anonymous | Login | Signup for a new account | 2019-02-22 02:17 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
0001908 | Frama-C | Plug-in > Eva | public | 2014-08-08 17:14 | 2015-03-17 22:18 | ||||
Reporter | Anne | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | OS Version | |||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Sodium | |||||||
Summary | 0001908: Non terminating call to stncpy | ||||||||
Description | I get a NON TERMINATING FUNCTION on the attached example due to a call to strncpy, but I don't really understand why... I added a \from part to the assigns property to remove the : warning: no \from part for clause 'assigns But it was not the problem. The message are: no state left in which to evaluate postcondition I didn't even found a workaround :-( | ||||||||
Steps To Reproduce | $ frama-c -val strncpy.c -cpp-extra-args="-I$(frama-c -print-share-path)/libc" - val-builtin strlen:Frama_C_strlen | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0005404) yakobowski (manager) 2014-08-08 21:09 |
Actually, the missing \from clauses are the culprit. Even with your addition, 'assigns \result \from dest' is still missing. Without it, '\result' gets assigned a default value that makes the postcondition '\result == dest' completely invalid. I will harden the message about '\from' clauses further, so that it also detects missing '\return' clauses. Concerning string.h, a patch that adds all the missing 'assigns' would be gladly accepted. |
(0005406) Anne (reporter) 2014-08-11 08:14 |
I am very sorry : I should have noticed that ! :-( About string.h, I'll have a look at it. |
(0005475) yakobowski (manager) 2014-09-19 16:32 |
Fix committed to master branch. |
![]() |
|||
Date Modified | Username | Field | Change |
2014-08-08 17:14 | Anne | New Issue | |
2014-08-08 17:14 | Anne | Status | new => assigned |
2014-08-08 17:14 | Anne | Assigned To | => yakobowski |
2014-08-08 17:14 | Anne | File Added: strncpy.c | |
2014-08-08 21:09 | yakobowski | Note Added: 0005404 | |
2014-08-11 08:14 | Anne | Note Added: 0005406 | |
2014-09-19 16:32 | yakobowski | Note Added: 0005475 | |
2014-09-19 16:32 | yakobowski | Status | assigned => resolved |
2014-09-19 16:32 | yakobowski | Resolution | open => fixed |
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
2015-03-17 22:18 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
Copyright © 2000 - 2019 MantisBT Team |