Frama-C Bug Tracking System - Frama-C
View Issue Details
0001013Frama-CKernelpublic2011-11-10 00:422012-09-19 17:16
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001013: Crash when casting something to type void
DescriptionThe 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.
TagsNo tags attached.
Attached Files

Notes
(0002460)
pascal   
2011-11-10 06:38   
An lvalue of type void should be a fatal error at parsing.
(0002464)
yakobowski   
2011-11-10 16:47   
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?
(0002466)
yakobowski   
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   
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   
2011-11-14 15:19   
This should indeed be a type error.
(0002473)
yakobowski   
2011-11-14 16:25   
Fixed in revision 16087

Issue History
2011-11-10 00:42yakobowskiNew Issue
2011-11-10 06:38pascalNote Added: 0002460
2011-11-10 16:47yakobowskiNote Added: 0002464
2011-11-10 17:38pascalNote Added: 0002465
2011-11-10 21:26yakobowskiNote Added: 0002466
2011-11-11 05:01pascalNote Added: 0002467
2011-11-14 15:19virgileNote Added: 0002471
2011-11-14 15:19virgileAssigned To => yakobowski
2011-11-14 15:19virgileStatusnew => confirmed
2011-11-14 16:25yakobowskiNote Added: 0002473
2011-11-14 16:25yakobowskiStatusconfirmed => resolved
2011-11-14 16:25yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed