Frama-C Bug Tracking System

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

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-09-02 12:49 monate New Issue
2011-09-02 12:49 monate Status new => assigned
2011-09-02 12:49 monate Assigned To => pascal
2011-09-02 21:18 monate Status assigned => resolved
2011-09-02 21:18 monate Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker