Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001013Frama-CKernelpublic2012-09-19 17:16
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0002460

pascal (reporter)

An lvalue of type void should be a fatal error at parsing.

~0002464

yakobowski (manager)

What about an expression?

~0002465

pascal (reporter)

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

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)

src[i] is an lvalue, which is exactly why it should not be allowed to be of type void.

~0002471

virgile (developer)

This should indeed be a type error.

~0002473

yakobowski (manager)

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