From 1e8e4fe745b8d0ccc1cb11b685d4068f7bb1a15a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 5 Sep 2023 16:08:28 +0200
Subject: [PATCH] [libc] improve stub for getline()
---
share/libc/stdio.c | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 2 +-
tests/libc/oracle/stdio_c.res.oracle | 6 +++---
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/share/libc/stdio.c b/share/libc/stdio.c
index 4aeab242231..1a59d873156 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 f54c0e53e9e..bc1a0874a6a 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 511866c32d3..b690ae42177 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.
--
GitLab