Crash when casting something to type void
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.