Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002310Frama-CPlug-in > E-ACSLpublic2017-06-13 11:082017-06-14 07:55
Reporterkvorobyov 
Assigned Tokvorobyov 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002310: Incorrect handling of \initialized when initialized struct is passed to a function by value
DescriptionThis test case is derived from Toyota ITC benchmarks (File uninit_var.c, test case 012). Consider the following code:

struct S1 {
  int t;
};

int foo(struct S1 s) {
  /*@assert \initialized(&s.t); */
  if (s.t > 0) return 0;
  return 1;
}

int main(int argc, const char **argv) {
  struct S1 s;
  s.t = 1;
  foo(s);
  return 0;
}

Field `t` of struct `S1` is initialized in `main` but when it is passed to `foo` (by value) it's a brand new block where field `t` is not marked as initialized. Consequently assertion in `foo` wrongly fails.
TagsNo tags attached.
Attached Filesc file icon itc-uninit-var-12.c [^] (252 bytes) 2017-06-13 11:08 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-06-13 11:08 kvorobyov New Issue
2017-06-13 11:08 kvorobyov Status new => assigned
2017-06-13 11:08 kvorobyov Assigned To => kvorobyov
2017-06-13 11:08 kvorobyov File Added: itc-uninit-var-12.c


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker