0001013: Crash when casting something to type void

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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.

Attached Files

Relationships

Notes
(0002460) pascal (reporter) 2011-11-10 06:38	An lvalue of type void should be a fatal error at parsing.

(0002464) yakobowski (manager) 2011-11-10 16:47	What about an expression?

(0002465) 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?

(0002466) 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.

(0002467) 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.

(0002471) virgile (developer) 2011-11-14 15:19	This should indeed be a type error.

(0002473) yakobowski (manager) 2011-11-14 16:25	Fixed in revision 16087

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