Frama-C Bug Tracking System - Frama-C
View Issue Details
0001447Frama-CPlug-in > Evapublic2013-06-13 15:022014-03-13 15:57
Jochen 
yakobowski 
normalminoralways
closedfixed 
Frama-C Fluorine-20130501 
Frama-C Neon-20140301 
0001447: uninitialized value can be passed through pointer, through return, but not through function argument
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.
No tags attached.
c ftest.c (229) 2013-06-13 15:02
https://bts.frama-c.com/file_download.php?file_id=505&type=bug
Issue History
2013-06-13 15:02JochenNew Issue
2013-06-13 15:02JochenStatusnew => assigned
2013-06-13 15:02JochenAssigned To => yakobowski
2013-06-13 15:02JochenFile Added: ftest.c
2013-06-15 18:56yakobowskiNote Added: 0003965
2013-06-19 21:50pascalNote Added: 0003973
2013-07-04 19:02svnCheckin
2013-11-05 23:06svnCheckin
2013-11-14 18:13svnCheckin
2013-11-14 18:13svnStatusassigned => resolved
2013-11-14 18:13svnResolutionopen => fixed
2013-11-14 18:21yakobowskiNote Added: 0004265
2014-02-12 16:57yakobowskiNote Added: 0004551
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0003965)
yakobowski   
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); }
(0003973)
pascal   
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.
(0004265)
yakobowski   
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.
(0004551)
yakobowski   
2014-02-12 16:57   
Fix committed to stable/neon branch.