0001447: uninitialized value can be passed through pointer, through return, but not through function argument

Notes
(0003965) 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); }

(0003973) 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.

(0004265) 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.

(0004551) yakobowski (manager) 2014-02-12 16:57	Fix committed to stable/neon branch.

Issue History
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	Checkin
2013-11-05 23:06	svn	Checkin
2013-11-14 18:13	svn	Checkin
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
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

Relationships