From a7f6aa882aa598fd82205772533ef515550aa961 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 24 Aug 2021 16:36:49 +0200
Subject: [PATCH] [Libc] add missing issues and improve test

---
 share/libc/__fc_libc.h                 |  5 ++++
 tests/libc/check_full_libc.sh          | 40 +++++++++++++++++---------
 tests/libc/fc_libc.c                   |  5 +++-
 tests/libc/oracle/fc_libc.0.res.oracle |  7 +++--
 tests/libc/oracle/fc_libc.1.res.oracle |  3 ++
 tests/libc/oracle/fc_libc.5.res.oracle |  3 --
 6 files changed, 43 insertions(+), 20 deletions(-)
 delete mode 100644 tests/libc/oracle/fc_libc.5.res.oracle

diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 6e43667ac7d..70797ab496b 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -28,9 +28,11 @@
 #define _GNU_SOURCE 1
 
 #include "alloca.h"
+#include "argz.h"
 #include "arpa/inet.h"
 #include "assert.h"
 #include "byteswap.h"
+//#include "complex.h"
 #include "ctype.h"
 #include "dirent.h"
 #include "dlfcn.h"
@@ -93,6 +95,7 @@
 #include "sys/signal.h"
 #include "sys/socket.h"
 #include "sys/stat.h"
+#include "sys/statvfs.h"
 #include "sys/time.h"
 #include "sys/times.h"
 #include "sys/timex.h"
@@ -100,8 +103,10 @@
 #include "sys/uio.h"
 #include "sys/un.h"
 #include "sys/utsname.h"
+#include "sys/vfs.h"
 #include "sys/wait.h"
 #include "termios.h"
+//#include "tgmath.h"
 #include "time.h"
 #include "unistd.h"
 #include "utime.h"
diff --git a/tests/libc/check_full_libc.sh b/tests/libc/check_full_libc.sh
index ebfc06b481c..7725be701da 100755
--- a/tests/libc/check_full_libc.sh
+++ b/tests/libc/check_full_libc.sh
@@ -1,17 +1,31 @@
-#!/bin/sh
+#!/bin/sh -eu
+
+errors=0
 
 cd share/libc
 
-for A in `ls *.h */*.h`;
-do
-    if ! grep -q $A ../../tests/libc/fc_libc.c ;
-    then echo "#include \"$A"\";
-    fi ;
-done;
+for A in *.h */*.h; do
+    if ! grep -q $A ../../tests/libc/fc_libc.c
+    then
+        echo "missing include in tests/libc/fc_libc.c: $A"
+        errors=$((errors+1))
+    fi
+    if ! grep -q $A __fc_libc.h && [ "${A#__fc_}" = "$A" ]
+    then
+        echo "missing include in share/libc/__fc_libc.h: $A"
+        errors=$((errors+1))
+    fi
+done
+
+for A in *.c */*.c; do
+    if ! grep -q $A __fc_runtime.c ../../tests/libc/fc_libc.c
+    then
+        echo "missing include in share/libc/__fc_runtime.c or tests/libc/fc_libc.c: $A"
+        errors=$((errors+1))
+    fi
+done
 
-for A in `ls *.c`;
-do
-    if ! grep -q $A __fc_runtime.c ../../tests/libc/fc_libc.c ;
-    then echo Not included implementation \'$A\';
-    fi ;
-done;
+if [ $errors -gt 0 ]; then
+    echo "found $errors error(s) in libc"
+    exit 1
+fi
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 51926233b9a..1345145e950 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -52,6 +52,7 @@
 #include "__fc_define_intptr_t.h"
 #include "__fc_define_iovec.h"
 #include "__fc_define_key_t.h"
+#include "__fc_define_max_open_files.h"
 #include "__fc_define_mode_t.h"
 #include "__fc_define_nlink_t.h"
 #include "__fc_define_null.h"
@@ -75,8 +76,10 @@
 #include "__fc_define_wint_t.h"
 #include "__fc_gcc_builtins.h"
 #include "__fc_inet.h"
+#include "__fc_integer.h"
+//#include "__fc_libc.h" //keep this; used by check_full_libc.sh
 #include "__fc_machdep.h"
-//#include "__fc_machdep_linux_shared.h"
+//#include "__fc_machdep_linux_shared.h" //keep this; used by check_full_libc.sh
 #include "fcntl.h"
 #include "__fc_select.h"
 #include "__fc_string_axiomatic.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 6278f20effa..a6771559129 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/libc/fc_libc.c:161: assertion got status valid.
-[eva] tests/libc/fc_libc.c:162: assertion got status valid.
-[eva] tests/libc/fc_libc.c:163: assertion got status valid.
 [eva] tests/libc/fc_libc.c:164: assertion got status valid.
+[eva] tests/libc/fc_libc.c:165: assertion got status valid.
+[eva] tests/libc/fc_libc.c:166: assertion got status valid.
+[eva] tests/libc/fc_libc.c:167: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -212,6 +212,7 @@
 #include "__fc_builtin.h"
 #include "__fc_define_fd_set_t.h"
 #include "__fc_gcc_builtins.h"
+#include "__fc_integer.h"
 #include "__fc_select.h"
 #include "alloca.h"
 #include "argz.c"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6fb5f06d16b..0bd9434fdce 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8033,6 +8033,9 @@ int __builtin_popcountl(unsigned long x);
  */
 int __builtin_popcountll(unsigned long long x);
 
+/*@ logic 𝔹 bit_test(ℤ x, ℤ pos) = (x & (1 << pos)) ≢ 0;
+
+*/
 /*@ requires valid_filename: valid_read_string(filename);
     assigns \result;
     assigns \result \from (indirect: *(filename + (0 ..))), (indirect: mode);
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
deleted file mode 100644
index 7e6030e3554..00000000000
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "__fc_define_max_open_files.h"
-#include "__fc_integer.h"
-#include "__fc_libc.h"
-- 
GitLab