C library: Do not require stdin, stdout, stderr to be initialised #4283
Conversation
vfprintf and several other library functions dereference a FILE*-typed stream parameter to make sure pointer checks and bounds checks are triggered. As we do not set up stdin, stdout, stderr to point to valid FILE-typed objects, make sure we never attempt such dereferencing if the stream argument is stdin/stdout/stderr (unless the use of any of those would in itself constitute an error, as is the case in fseek, for example).
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 3f1ea29).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102412913
src/ansi-c/library/stdio.c
Outdated
| @@ -379,20 +391,27 @@ int __VERIFIER_nondet_int(); | |||
|
|
|||
| inline int fileno(FILE *stream) | |||
| { | |||
| // just return nondet | |||
| __CPROVER_HIDE:; | |||
| // just return nondet | |||
There was a problem hiding this comment.
This comment seems out of place now
|
Should we instead initialize them? is valid. |
| return 1; | ||
| else if(stream == stderr) | ||
| return 2; | ||
|
|
There was a problem hiding this comment.
As long as stdin etc. are uninitialised, the above returns may all be executed.
There was a problem hiding this comment.
I'm working on a follow-up PR to initialise them.
| (void)*stream; | ||
| #else | ||
| (void)*(char *)stream; | ||
| #endif |
There was a problem hiding this comment.
I think the VCCs get a bit easier if the type matches that of the allocation.
There was a problem hiding this comment.
Yes, but that (__linux__ && !__GLIBC__) is the case where FILE remains an incomplete type.
The earlier commit made sure it returns 0/1/2 for stdin/stdout/stderr.
Note the missing "R".
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 92a3802).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102475281
vfprintf and several other library functions dereference a FILE*-typed stream
parameter to make sure pointer checks and bounds checks are triggered. As we do
not set up stdin, stdout, stderr to point to valid FILE-typed objects, make sure
we never attempt such dereferencing if the stream argument is
stdin/stdout/stderr (unless the use of any of those would in itself constitute
an error, as is the case in fseek, for example).