Frama-C Bug Tracking System - Frama-C
View Issue Details
0002310Frama-CPlug-in > E-ACSLpublic2017-06-13 11:082019-01-25 10:54
kvorobyov 
signoles 
normalminoralways
assignedopen 
 
 
0002310: Incorrect handling of \initialized when initialized struct is passed to a function by value
This 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.
No tags attached.
c itc-uninit-var-12.c (252) 2017-06-13 11:08
https://bts.frama-c.com/file_download.php?file_id=1190&type=bug
Issue History
2017-06-13 11:08kvorobyovNew Issue
2017-06-13 11:08kvorobyovStatusnew => assigned
2017-06-13 11:08kvorobyovAssigned To => kvorobyov
2017-06-13 11:08kvorobyovFile Added: itc-uninit-var-12.c
2017-10-24 17:42signolesAssigned Tokvorobyov => signoles
2018-02-22 10:32signolesAssigned Tosignoles => fmaurica
2018-09-14 14:21signolesTarget Version => Frama-C 18-Argon
2018-10-02 13:25signolesTarget VersionFrama-C 18-Argon =>
2019-01-25 10:54signolesAssigned Tofmaurica => signoles

There are no notes attached to this issue.