Frama-C Bug Tracking System - Frama-C
View Issue Details
0000949Frama-CPlug-in > Evapublic2011-09-02 12:492011-10-10 14:14
Reportermonate 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFrama-C GIT, precise the release idFixed in VersionFrama-C Nitrogen-20111001 
Summary0000949: Valid access to literal w_chart string address considered invalid
Description#include <stddef.h>

int main() {

  // String literals are lvalues
  char (*p)[4] = &("bar");
  wchar_t (*q)[4] = &(L"foO");

  if((*p)[1] != 'a') return 1;
  if((*q)[1] != 'o') return 2;
  
  return 0;
}

return 0 when gcc'ed but frama-c -val ends with
tests/cil/string.c:10:[kernel] warning: out of bounds read. assert \valid(&(*q)[1]);
TagsNo tags attached.
Attached Files

There are no notes attached to this issue.

Issue History
2011-09-02 12:49monateNew Issue
2011-09-02 12:49monateStatusnew => assigned
2011-09-02 12:49monateAssigned To => pascal
2011-09-02 21:18monateStatusassigned => resolved
2011-09-02 21:18monateResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva