GitLab

ID0000913: This issue was created automatically from Mantis Issue 913. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000913	Frama-C	Plug-in > Eva	public	2011-08-05	2011-10-10

Reporter	yakobowski	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

A precise assigns clause for function memcpy is /@ assigns ((char)dst)[0..n] \from ((char*)src)[0..n]; assigns \result \from dst; / void Frama_C_memcpy(void* dst, const void* src, unsigned n);

This is currently not treated by the aforementioned Db function, probably because of the casts to char*. By using char* directly everywhere, the assigns clause is (imprecisely) translated to something equivalent to /*@ assigns dst[..] \from src[..];

Since the comment on the function is to complain if some unsupported cases are required, I'm complaining :-)