Skip to content

Commit 25a71fc

Browse files
committed
C library/fread: use __VERIFIER_nondet_char
The uninitialised local variable can trip up GCC's validation. Use a __VERIFIER_nondet_ function as is already done elsewhere.
1 parent 1a355b6 commit 25a71fc

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/ansi-c/library/stdio.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,7 @@ char *fgets(char *str, int size, FILE *stream)
330330
#define __CPROVER_STDIO_H_INCLUDED
331331
#endif
332332

333+
char __VERIFIER_nondet_char();
333334
size_t __VERIFIER_nondet_size_t();
334335

335336
inline size_t fread(
@@ -359,8 +360,7 @@ inline size_t fread(
359360

360361
for(size_t i=0; i<bytes; i++)
361362
{
362-
char nondet_char;
363-
((char *)ptr)[i]=nondet_char;
363+
((char *)ptr)[i] = __VERIFIER_nondet_char();
364364
}
365365

366366
return nread;

0 commit comments

Comments
 (0)