Non terminating call to stncpy
ID0001908: This issue was created automatically from Mantis Issue 1908. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001908 | Frama-C | Plug-in > Eva | public | 2014-08-08 | 2015-03-17 |
Reporter | Anne | Assigned To | yakobowski | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | have not tried |
Platform | - | OS | - | OS Version | - |
Product Version | - | Target Version | - | Fixed in Version | Frama-C Sodium |
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