Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001013 | Frama-C | Kernel | public | 2011-11-10 00:42 | 2012-09-19 17:16 |
|
| Reporter | yakobowski | |
|---|
| Assigned To | yakobowski | |
|---|
| Priority | normal | Severity | crash | Reproducibility | always |
|---|
| Status | closed | Resolution | fixed | |
|---|
| Platform | | OS | | OS Version | |
|---|
| Product Version | Frama-C Nitrogen-20111001 | |
|---|
| Target Version | | Fixed in Version | Frama-C Oxygen-20120901 | |
|---|
|
| Summary | 0001013: Crash when casting something to type void |
|---|
| 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. |
|---|
| Tags | No tags attached. |
|---|
| Relationships | |
| Attached Files | |
|---|
|
Notes |
|
|
(0002460)
|
|
pascal
|
|
2011-11-10 06:38
|
|
|
An lvalue of type void should be a fatal error at parsing. |
|
|
|
|
|
What about an expression? |
|
|
|
(0002465)
|
|
pascal
|
|
2011-11-10 17:38
|
|
> What about an expression?
Good question. Let's work it out:
void f(int);
What is the type of the C expression f(0) and do we want to forbid such expressions? |
|
|
|
|
|
Tsss, I meant an expression such as src[i] here (whose analysis proceeds at least during a few microseconds because we allow the computation of sizeof(void)). Anyways, we should reject everything. |
|
|
|
(0002467)
|
|
pascal
|
|
2011-11-11 05:01
|
|
|
src[i] is an lvalue, which is exactly why it should not be allowed to be of type void. |
|
|
|
|
|
This should indeed be a type error. |
|
|
|
|
|