diff --git a/share/libc/stdio.c b/share/libc/stdio.c index 4aeab242231de4785fcfa77d8af426e61674df6a..1a59d87315602df554006108714350d5edf61d46 100644 --- a/share/libc/stdio.c +++ b/share/libc/stdio.c @@ -71,7 +71,7 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream) { } if (!*lineptr || *n == 0) { *lineptr = malloc(2); - if (!lineptr) { + if (!*lineptr) { errno = ENOMEM; //TODO: set error indicator for stream return -1; diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index f54c0e53e9ef9e9077a8f8d192babb74943146b3..bc1a0874a6a93bd9e5e05847cfa88d8d8b87858c 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -6594,7 +6594,7 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream) _LOR_1: { *lineptr = (char *)malloc((size_t)2); - if (! lineptr) { + if (! *lineptr) { __fc_errno = 12; __retres = -1; goto return_label; diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle index 511866c32d3bbdf6538340b08ffa394af13879a9..b690ae421776ff0d02c2d2880b6660d6d1d7a495 100644 --- a/tests/libc/oracle/stdio_c.res.oracle +++ b/tests/libc/oracle/stdio_c.res.oracle @@ -64,9 +64,6 @@ [eva] Done for function Frama_C_unsigned_char_interval [eva] Recording results for fgetc [eva] Done for function fgetc -[eva:alarm] FRAMAC_SHARE/libc/stdio.c:90: Warning: - out of bounds write. assert \valid(*lineptr + tmp_2); - (tmp_2 from cur++) [eva] FRAMAC_SHARE/libc/stdio.c:83: starting to merge loop iterations [eva] FRAMAC_SHARE/libc/stdio.c:84: Reusing old results for call to fgetc [eva] FRAMAC_SHARE/libc/stdio.c:104: Call to builtin realloc @@ -90,6 +87,9 @@ Called from FRAMAC_SHARE/libc/stdio.c:82. [eva] Done for function feof [eva] FRAMAC_SHARE/libc/stdio.c:84: Reusing old results for call to fgetc +[eva:alarm] FRAMAC_SHARE/libc/stdio.c:90: Warning: + out of bounds write. assert \valid(*lineptr + tmp_2); + (tmp_2 from cur++) [eva] FRAMAC_SHARE/libc/stdio.c:84: Reusing old results for call to fgetc [eva] FRAMAC_SHARE/libc/stdio.c:104: Call to builtin realloc [eva] computing for function ferror <- getline <- main.