Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001447Frama-CPlug-in > Evapublic2013-06-13 15:022014-03-13 15:57
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001447: uninitialized value can be passed through pointer, through return, but not through function argument
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (229 bytes) 2013-06-13 15:02 [Show Content]

- Relationships

-  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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker