GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0001000	Frama-C	Plug-in > Eva	public	2011-10-25	2014-02-12

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

Description :

Evaluation in the logic sometimes causes the warning "using size of void". Worse, this can lead to crashes, as e.g. do_cast raises assert false when it encounters something of type void.

It is not clear how one goes from something that has type void* to something that has type void, but this definitely happens.

Steps To Reproduce :

This example can be used to cause the apparition of the warning

frama-c -val -then -print

void main (int i) { int x=1; while(1) Frama_C_memcpy((void )&x, (void const)&x, i); }

The generated assertion cast the pointer to void*, then does arithmetic on it. This is incorrect.