| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| 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 | ||||||
| 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. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pascal (reporter) 2011-11-10 06:38 |
An lvalue of type void should be a fatal error at parsing. |
|
yakobowski (manager) 2011-11-10 16:47 |
What about an expression? |
|
pascal (reporter) 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? |
|
yakobowski (manager) 2011-11-10 21:26 |
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. |
|
pascal (reporter) 2011-11-11 05:01 |
src[i] is an lvalue, which is exactly why it should not be allowed to be of type void. |
|
virgile (developer) 2011-11-14 15:19 |
This should indeed be a type error. |
|
yakobowski (manager) 2011-11-14 16:25 |
Fixed in revision 16087 |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-11-10 00:42 | yakobowski | New Issue | |
| 2011-11-10 06:38 | pascal | Note Added: 0002460 | |
| 2011-11-10 16:47 | yakobowski | Note Added: 0002464 | |
| 2011-11-10 17:38 | pascal | Note Added: 0002465 | |
| 2011-11-10 21:26 | yakobowski | Note Added: 0002466 | |
| 2011-11-11 05:01 | pascal | Note Added: 0002467 | |
| 2011-11-14 15:19 | virgile | Note Added: 0002471 | |
| 2011-11-14 15:19 | virgile | Assigned To | => yakobowski |
| 2011-11-14 15:19 | virgile | Status | new => confirmed |
| 2011-11-14 16:25 | yakobowski | Note Added: 0002473 | |
| 2011-11-14 16:25 | yakobowski | Status | confirmed => resolved |
| 2011-11-14 16:25 | yakobowski | Resolution | open => fixed |
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| Issue History |