uninitialized value can be passed through pointer, through return, but not through function argument
ID0001447: This issue was created automatically from Mantis Issue 1447. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001447 | Frama-C | Plug-in > Eva | public | 2013-06-13 | 2014-03-13 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130501 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
Running "frama-c -val ftest.c" on the attached program doesn't produce any warning, although the uninitialized value of variable "undf" is passed to variable "i" and "k" via assignment to a pointer and via return in line 7 and 9, respectively.
If it is passed also to variable "j" via function argument (uncomment line 8 to do this), a warning is issued, as expected, even although "j" is never used.
I would have expected similar behavior in all 3 cases, preferrable issuing always a warning.