Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

- 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker