View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001447 | Frama-C | Plug-in > Eva | public | 2013-06-13 15:02 | 2014-03-13 15:57 | ||||
Reporter | Jochen | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Fluorine-20130501 | ||||||||
Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
Summary | 0001447: uninitialized value can be passed through pointer, through return, but not through function argument | ||||||||
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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2013-06-15 18:56 |
The treatment of unitialized values is a bit of a grey area, but I tend to agree that all three lines should result in the same behavior. I'm going to see with Pascal what is his opinion on this matter, though. (Notice that the warning will be emitted only for fully unitialized values. In the variant below, no alarm is emitted on use(undef). Value never warns on partially unitialized values to account for the possibility of padding bits.) void use(int j) { } void f(int *p) { int undf; *((char*)&undf) = 1; use(undf); // pass by (unused) fct arg } void main(void) { int i; f(&i); } |
pascal (reporter) 2013-06-19 21:50 |
Behavior wrt indeterminate memory in argument-passing is the result of negotiations with paying customers to find the compromise that was just right for them. They won't like it if we change it. The current behavior in assignments is necessary to handle programs that blit structures or unions (containing uninitialized padding), for instance memcpy() The current behavior for function returns has not been challenged until now. Note that in all three cases, the alarm is only postponed until the value is used (and if the uninitialized value is not used, it wasn't too dangerous in the first place, although it may still be Undefined Behavior according to the standard). I seem to remember that CompCert's authors decided to copy our choice for assignments. Another thing I remember is that an exception to what I just said is passing indeterminate memory to functions whose code is unavailable. Then one may not notice the error that happens inside the function. But there are special cases in the implementation precisely to be stricter for arguments passed to library functions, for this reason. ____ I vote to avoid changing anything regarding the treatment of indeterminate memory. |
yakobowski (manager) 2013-11-14 18:21 |
The handling of unitialized values being copied will change in Neon. With the default options, all three lines of your example will be accepted. With option "-val-warn-copy-indeterminate *", they will all be rejected. |
yakobowski (manager) 2014-02-12 16:57 |
Fix committed to stable/neon branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-06-13 15:02 | Jochen | New Issue | |
2013-06-13 15:02 | Jochen | Status | new => assigned |
2013-06-13 15:02 | Jochen | Assigned To | => yakobowski |
2013-06-13 15:02 | Jochen | File Added: ftest.c | |
2013-06-15 18:56 | yakobowski | Note Added: 0003965 | |
2013-06-19 21:50 | pascal | Note Added: 0003973 | |
2013-07-04 19:02 | svn | ||
2013-11-05 23:06 | svn | ||
2013-11-14 18:13 | svn | ||
2013-11-14 18:13 | svn | Status | assigned => resolved |
2013-11-14 18:13 | svn | Resolution | open => fixed |
2013-11-14 18:21 | yakobowski | Note Added: 0004265 | |
2013-12-19 01:11 | yakobowski | Source_changeset_attached | => framac master a475e848 |
2013-12-19 01:11 | yakobowski | Source_changeset_attached | => framac master 2a3c5d57 |
2014-02-12 16:53 | yakobowski | Source_changeset_attached | => framac stable/neon a475e848 |
2014-02-12 16:53 | yakobowski | Source_changeset_attached | => framac stable/neon 2a3c5d57 |
2014-02-12 16:57 | yakobowski | Note Added: 0004551 | |
2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
2014-03-13 15:57 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |