GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0001013	Frama-C	Kernel	public	2011-11-10	2012-09-19

Reporter	yakobowski	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Nitrogen-20111001	Target Version	-	Fixed in Version	Frama-C Oxygen-20120901

Description :

The value analysis crashes on the following code, analyzed with -val

void* memcpy(void* dst, const void *src, unsigned long n) { for (int i=0;i<n;i++) dst[i]=src[i]; return dst; }

void main () { int x = 1; memcpy(&x,&x,4); }

Casting src[i] to type void causes a crash. We have two possibilities here:

• add a fatal error during parsing, when something has type void. This is what gcc does, and in my opinion the best solution;
• change the 'assert false' inside the value analysis into something else, probably a fatal user error.