Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001908Frama-CPlug-in > Evapublic2014-08-08 17:142015-03-17 22:18
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001908: Non terminating call to stncpy
DescriptionI 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
TagsNo tags attached.
Attached Filesc file icon strncpy.c [^] (615 bytes) 2014-08-08 17:14 [Show Content]

- Relationships

-  Notes
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.
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.
yakobowski (manager)
2014-09-19 16:32

Fix committed to master branch.

- Issue History
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker