Incorrect handling of \initialized when initialized struct is passed to a function by value
ID0002310: This issue was created automatically from Mantis Issue 2310. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002310 | Frama-C | Plug-in > E-ACSL | public | 2017-06-13 | 2019-01-25 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information