0000718: possible unsoundness in r11866 - Frama-C Bug Tracking System

Notes
(0001483) pascal (reporter) 2011-02-13 00:14 edited on: 2011-02-13 00:16	The proper message (including the word "assert") is missing from the output, but the value analysis has found that g_23 could be 9 at some point, and has then cut that branch because it lead to guaranteed undefined behavior: [value] computing for function func_42 <-func_1 <-main. Called from foo.c:71. [value] Recording results for func_42 foo.c:140:[value] warning: local escaping the scope of func_42 through \result [value] Done for function func_42 foo.c:71:[kernel] warning: completely undefined value in {{ tmp_9 -> {0; } ;}} (size:<32>). [value] Recording results for func_1 [value] Done for function func_1 func_42 returns the address of a local variable: int32_t func_42(int8_t p_43, uint32_t p_44, int32_t p_45, uint32_t p_46) { const int64_t l_61 = 0xB4954824FF24264ALL; int32_t l_64 = &g_30; int8_t l_120 = 0xE3L; uint64_t l_121 = -2L; uint8_t l_122 = 1L; int32_t l_123 = &l_64; (*g_21) \|= l_120; return l_123; } The address, that it is illegal to use, returned by the first call is passed as an argument on the second call to func_42. This is when the value analysis warns as above and stops propagation. We can argue about the precise place the warning should be (we do not want to stop propagation when a global has contained the address of a local but is no longer accessed after the function returns), but this program contains an undefined behavior. I will add an explicit message with the word "assert" for the case where the variable with undefined contents is passed as an argument to another function.

(0001484) pascal (reporter) 2011-02-13 01:14	This example now emits the warning: foo.c:71:[kernel] warning: accessing left-value tmp_9 that contains escaping addresses; assert(Ook) I believe this is the path that is followed by the real execution. Removing the "volatile"s would probably confirm this.

(0001486) regehr (reporter) 2011-02-13 05:29	n1124 says: "If an object is referred to outside of its lifetime, the behavior is undefined. The value of a pointer becomes indeterminate when the object it points to reaches the end of its lifetime." Permitting a pointer to escape doesn't constitute "referring to", which would require a dereference operation. Therefore our reading is that it's OK to permit pointers to escape as long as they are not subsequently used, and we deliberately coded Csmith to generate programs that do this.

(0001487) regehr (reporter) 2011-02-13 05:30	Hmm, I was going to re-close this issue after making the previous comment, but I can't seem to -- perhaps only maintainers have privileges to do that? Anyway my intent wasn't to try to keep this bug alive, but rather to add the note about our reading of the C99 standard.

(0001489) pascal (reporter) 2011-02-13 07:13	"indeterminate" is also defined as "either an unspecified value or a trap representation". J.2. defines a case of undefined behavior as "A trap representation is read by an lvalue expression that does not have character type (6.2.6.1).". The words "trap representation" are more or less defined by example in 6.2.6.1.5. This said, I thought you were going to argue for having the warning sooner, not later. The alarm had been forgotten because warning for a completely undefined lvalue as argument for a function was a separate feature. The value analysis avoids warning for partially undefined lvalues because structs (which can be passed as arguments) always contain undefined padding or fields that it does not make sense to initialize in some cases. The "warn for completely undefined argument" requirement was expressed by a user; we implemented it without an option to select the behavior, and no-one until now complained that they wanted to pass dangling pointers as parameters to functions without warning. Architecturally, it would be very easy to wait until the program does pointer arithmetic on (or of course dereferences) the dangling pointer to emit the alarm. We are emitting it early as a favor.

(0004834) pascal (reporter) 2014-02-12 16:59	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-02-12 23:43	regehr	New Issue
2011-02-12 23:43	regehr	Status	new => assigned
2011-02-12 23:43	regehr	Assigned To	=> pascal
2011-02-12 23:43	regehr	File Added: foo_pp.c
2011-02-13 00:14	pascal	Note Added: 0001483
2011-02-13 00:16	pascal	Note Edited: 0001483
2011-02-13 01:14	pascal	Note Added: 0001484
2011-02-13 01:15	svn	Checkin
2011-02-13 01:15	svn	Status	assigned => resolved
2011-02-13 01:15	svn	Resolution	open => fixed
2011-02-13 05:29	regehr	Note Added: 0001486
2011-02-13 05:29	regehr	Status	resolved => feedback
2011-02-13 05:29	regehr	Resolution	fixed => reopened
2011-02-13 05:30	regehr	Note Added: 0001487
2011-02-13 07:13	pascal	Note Added: 0001489
2011-02-13 07:13	pascal	Status	feedback => resolved
2011-02-13 07:13	pascal	Resolution	reopened => fixed
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2014-02-12 16:59	pascal	Note Added: 0004834
2014-02-12 16:59	pascal	Status	closed => resolved
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Relationships