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

Attachments

• strncpy.c