Non terminating call to stncpy
ID0001908: This issue was created automatically from Mantis Issue 1908. Further discussion may take place here.
|ID0001908||Frama-C||Plug-in > Eva||public||2014-08-08||2015-03-17|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Product Version||-||Target Version||-||Fixed in Version||Frama-C Sodium|
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