diff --git a/Makefile b/Makefile
index 62da0160b06b00127cd4a487da4e77d2e5a8486b..5c8a9a2b9f15054e4fd3e7219bba502eef91cc87 100644
--- a/Makefile
+++ b/Makefile
@@ -188,7 +188,7 @@ THEME_ICONS_FLAT:= \
$(addprefix share/theme/flat/,$(THEME_ICON_NAMES))
ROOT_LIBC_DIR:= share/libc
-LIBC_SUBDIRS:= sys netinet linux net arpa
+LIBC_SUBDIRS:= sys netinet net arpa
LIBC_DIR:= $(ROOT_LIBC_DIR) $(addprefix $(ROOT_LIBC_DIR)/,$(LIBC_SUBDIRS))
LIBC_FILES:= \
$(wildcard share/*.h share/*.c) \
@@ -1874,7 +1874,6 @@ install:: install-lib
$(MKDIR) $(FRAMAC_DATADIR)/theme/flat
$(MKDIR) $(FRAMAC_DATADIR)/libc/sys
$(MKDIR) $(FRAMAC_DATADIR)/libc/netinet
- $(MKDIR) $(FRAMAC_DATADIR)/libc/linux
$(MKDIR) $(FRAMAC_DATADIR)/libc/net
$(MKDIR) $(FRAMAC_DATADIR)/libc/arpa
$(PRINT_INSTALL) shared files
@@ -1917,7 +1916,6 @@ install:: install-lib
$(CP) share/libc/arpa/*.[ch] $(FRAMAC_DATADIR)/libc/arpa
$(CP) share/libc/net/*.[ch] $(FRAMAC_DATADIR)/libc/net
$(CP) share/libc/netinet/*.[ch] $(FRAMAC_DATADIR)/libc/netinet
- $(CP) share/libc/linux/*.[ch] $(FRAMAC_DATADIR)/libc/linux
$(PRINT_INSTALL) binaries
$(CP) bin/toplevel.$(OCAMLBEST) $(BINDIR)/frama-c$(EXE)
$(CP) bin/toplevel.byte$(EXE) $(BINDIR)/frama-c.byte$(EXE)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 80fdaba048b40b8b8a639b45aa48a1aa6e8077dc..43be8eb708ab85c08c4cac5f985bcb17876bbc51 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -224,13 +224,7 @@ share/libc/inttypes.c: CEA_LGPL
share/libc/inttypes.h: CEA_LGPL
share/libc/iso646.h: CEA_LGPL
share/libc/libgen.h: CEA_LGPL
-share/libc/libintl.h: CEA_LGPL
share/libc/limits.h: CEA_LGPL
-share/libc/linux/fs.h: CEA_LGPL
-share/libc/linux/if_addr.h: CEA_LGPL
-share/libc/linux/if_netlink.h: CEA_LGPL
-share/libc/linux/netlink.h: CEA_LGPL
-share/libc/linux/rtnetlink.h: CEA_LGPL
share/libc/locale.c: CEA_LGPL
share/libc/locale.h: CEA_LGPL
share/libc/malloc.h: CEA_LGPL
@@ -243,9 +237,6 @@ share/libc/net/if.h: CEA_LGPL
share/libc/netdb.c: CEA_LGPL
share/libc/netdb.h: CEA_LGPL
share/libc/netinet/in.h: CEA_LGPL
-share/libc/netinet/in_systm.h: CEA_LGPL
-share/libc/netinet/ip.h: CEA_LGPL
-share/libc/netinet/ip_icmp.h: CEA_LGPL
share/libc/netinet/tcp.h: CEA_LGPL
share/libc/nl_types.h: CEA_LGPL
share/libc/poll.h: CEA_LGPL
@@ -273,7 +264,6 @@ share/libc/sys/file.h: CEA_LGPL
share/libc/sys/ioctl.h: CEA_LGPL
share/libc/sys/ipc.h: CEA_LGPL
share/libc/sys/mman.h: CEA_LGPL
-share/libc/sys/param.h: CEA_LGPL
share/libc/sys/random.h: CEA_LGPL
share/libc/sys/resource.h: CEA_LGPL
share/libc/sys/select.h: CEA_LGPL
@@ -281,7 +271,6 @@ share/libc/sys/shm.h: CEA_LGPL
share/libc/sys/signal.h: CEA_LGPL
share/libc/sys/socket.h: CEA_LGPL
share/libc/sys/stat.h: CEA_LGPL
-share/libc/sys/sysctl.h: CEA_LGPL
share/libc/sys/time.h: CEA_LGPL
share/libc/sys/times.h: CEA_LGPL
share/libc/sys/timex.h: CEA_LGPL
@@ -293,9 +282,8 @@ share/libc/sys/wait.h: CEA_LGPL
share/libc/syslog.h: CEA_LGPL
share/libc/termios.h: CEA_LGPL
share/libc/tgmath.h: CEA_LGPL
-share/libc/time.h: CEA_LGPL
share/libc/time.c: CEA_LGPL
-share/libc/uchar.h: CEA_LGPL
+share/libc/time.h: CEA_LGPL
share/libc/unistd.h: CEA_LGPL
share/libc/utime.h: CEA_LGPL
share/libc/utmpx.h: CEA_LGPL
diff --git a/share/libc/libgen.h b/share/libc/libgen.h
index 1abe66dd28cc3ebb3d7847b1ba63074c4296f798..1cfded11784bc2d799ac973f9f810aea06022a2f 100644
--- a/share/libc/libgen.h
+++ b/share/libc/libgen.h
@@ -20,13 +20,36 @@
/* */
/**************************************************************************/
-#ifndef __FC_LIBGEN
-#define __FC_LIBGEN
+#ifndef __FC_LIBGEN_H
+#define __FC_LIBGEN_H
#include "features.h"
+#include "__fc_machdep.h"
+#include "__fc_string_axiomatic.h"
__PUSH_FC_STDLIB
__BEGIN_DECLS
+extern char __fc_basename[__FC_PATH_MAX];
+char *__fc_p_basename = __fc_basename;
+
+/*@ // missing: assigns path[0 ..], __fc_p_basename[0 ..] \from 'filesystem';
+ requires null_or_valid_string_path: path == \null || valid_read_string(path);
+ assigns path[0 ..], __fc_basename[0 ..] \from path[0 ..], __fc_basename[0 ..];
+ assigns \result \from __fc_p_basename, path;
+ ensures result_points_to_internal_storage_or_path:
+ \subset(\result, {__fc_p_basename, path});
+*/
extern char *basename(char *path);
+
+extern char __fc_dirname[__FC_PATH_MAX];
+char *__fc_p_dirname = __fc_dirname;
+
+/*@ // missing: assigns path[0 ..], __fc_p_dirname[0 ..] \from 'filesystem';
+ requires null_or_valid_string_path: path == \null || valid_read_string(path);
+ assigns path[0 ..], __fc_dirname[0 ..] \from path[0 ..], __fc_dirname[0 ..];
+ assigns \result \from __fc_p_dirname, path;
+ ensures result_points_to_internal_storage_or_path:
+ \subset(\result, {__fc_p_dirname, path});
+*/
extern char *dirname(char *path);
__END_DECLS
diff --git a/share/libc/libintl.h b/share/libc/libintl.h
deleted file mode 100644
index f79f14d0fcfdb0482bfa524301ebc55a9f38eb53..0000000000000000000000000000000000000000
--- a/share/libc/libintl.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_LIBINTL_H
-#define __FC_LIBINTL_H
-
-#endif
diff --git a/share/libc/linux/fs.h b/share/libc/linux/fs.h
deleted file mode 100644
index c0b6d361f2d781309374dd3c9efcc86cd1d8196c..0000000000000000000000000000000000000000
--- a/share/libc/linux/fs.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_LINUX_FS_H
-#define __FC_LINUX_FS_H
-/* TODO */
-
-#endif
-
diff --git a/share/libc/linux/if_addr.h b/share/libc/linux/if_addr.h
deleted file mode 100644
index 51efee090ac1788a4db5851a27a04303a0efb0d5..0000000000000000000000000000000000000000
--- a/share/libc/linux/if_addr.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_LINUX_IF_ADDR_H
-#define __FC_LINUX_IF_ADDR_H
-
-#endif
diff --git a/share/libc/linux/if_netlink.h b/share/libc/linux/if_netlink.h
deleted file mode 100644
index 276d067832a672962cb593531e6b95205c857db2..0000000000000000000000000000000000000000
--- a/share/libc/linux/if_netlink.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_IF_NETLINK_H
-#define __FC_IF_NETLINK_H
-
-#endif
-
diff --git a/share/libc/linux/netlink.h b/share/libc/linux/netlink.h
deleted file mode 100644
index 1ddd191ab29e8419a1ef0dedfbcdbc6ac73c56ce..0000000000000000000000000000000000000000
--- a/share/libc/linux/netlink.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_LINUX_NETLINK_H
-#define __FC_LINUX_NETLINK_H
-
-
-
-#endif
diff --git a/share/libc/linux/rtnetlink.h b/share/libc/linux/rtnetlink.h
deleted file mode 100644
index 7ea2a119e9f92904ec8d82044c36b2eb89273995..0000000000000000000000000000000000000000
--- a/share/libc/linux/rtnetlink.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_LINUX_RTNETLINK_H
-#define __FC_LINUX_RTNETLINK_H
-
-
-#endif
-
diff --git a/share/libc/netinet/in_systm.h b/share/libc/netinet/in_systm.h
deleted file mode 100644
index 1beabb1cae1d68c9448bc06e4f4d61a4f0a9eb99..0000000000000000000000000000000000000000
--- a/share/libc/netinet/in_systm.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_NETINET_SYSTM_H
-#define __FC_NETINET_SYSTM_H
-
-#endif
diff --git a/share/libc/netinet/ip.h b/share/libc/netinet/ip.h
deleted file mode 100644
index 0c469cede7533dbba94f67cb2e601c6d585a8539..0000000000000000000000000000000000000000
--- a/share/libc/netinet/ip.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_NETINET_IP_H
-#define __FC_NETINET_IP_H
-
-#endif
diff --git a/share/libc/netinet/ip_icmp.h b/share/libc/netinet/ip_icmp.h
deleted file mode 100644
index 78e895961d9fba583731860cac67c0cee72f8e9e..0000000000000000000000000000000000000000
--- a/share/libc/netinet/ip_icmp.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_NETINET_IP_ICMP_H
-#define __FC_NETINET_IP_ICMP_H
-
-#endif
-
diff --git a/share/libc/sys/param.h b/share/libc/sys/param.h
deleted file mode 100644
index 93e55b1606cdcd6eeec17f095f0e59482a8a8729..0000000000000000000000000000000000000000
--- a/share/libc/sys/param.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_SYS_PARAM_H__
-#define __FC_SYS_PARAM_H__
-/* Only deprecated programs use this header. Add whatever is needed
- for this program to compile. */
-
-#endif
diff --git a/share/libc/sys/sysctl.h b/share/libc/sys/sysctl.h
deleted file mode 100644
index bd14e7820b752c14887790e628692ff83d7d4a87..0000000000000000000000000000000000000000
--- a/share/libc/sys/sysctl.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
diff --git a/share/libc/uchar.h b/share/libc/uchar.h
deleted file mode 100644
index 61011a2d979742edf859fbf2c054aa58c83d4023..0000000000000000000000000000000000000000
--- a/share/libc/uchar.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2019 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-/* ISO C: 7.24 */
-#ifndef __FC_UCHAR
-#define __FC_UCHAR
-
-#endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 298bc1b03740873f4764513b51d10747b6869bd3..5688d0e6e4f9e8c9ab57ab0ce3c62c2b9fdbdbd0 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -85,13 +85,7 @@
#include "inttypes.h"
#include "iso646.h"
#include "libgen.h"
-#include "libintl.h"
#include "limits.h"
-#include "linux/fs.h"
-#include "linux/if_addr.h"
-#include "linux/if_netlink.h"
-#include "linux/netlink.h"
-#include "linux/rtnetlink.h"
#include "locale.h"
#include "malloc.h"
#include "math.h"
@@ -99,9 +93,6 @@
#include "netdb.h"
#include "net/if.h"
#include "netinet/in.h"
-#include "netinet/in_systm.h"
-#include "netinet/ip.h"
-#include "netinet/ip_icmp.h"
#include "netinet/tcp.h"
#include "nl_types.h"
#include "poll.h"
@@ -127,7 +118,6 @@
#include "sys/ipc.h"
#include "syslog.h"
#include "sys/mman.h"
-#include "sys/param.h"
#include "sys/random.h"
#include "sys/resource.h"
#include "sys/select.h"
@@ -135,7 +125,6 @@
#include "sys/signal.h"
#include "sys/socket.h"
#include "sys/stat.h"
-#include "sys/sysctl.h"
#include "sys/time.h"
#include "sys/times.h"
#include "sys/timex.h"
@@ -147,7 +136,6 @@
#include "termios.h"
#include "tgmath.h"
#include "time.h"
-#include "uchar.h"
#include "unistd.h"
#include "utime.h"
#include "utmpx.h"
diff --git a/tests/libc/libgen_h.c b/tests/libc/libgen_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..df9e7eaf4c2e3f29d8f6deb6b76e7b5c4fb9fbab
--- /dev/null
+++ b/tests/libc/libgen_h.c
@@ -0,0 +1,20 @@
+/*run.config
+
+*/
+
+#include <libgen.h>
+
+int main() {
+ char path[128] = "/tmp/bla/ble.c";
+ char *base = basename(path);
+ //@ assert valid_string(base);
+ char *base2 = basename(0);
+ //@ assert valid_string(base2);
+
+ char *dir = dirname(path);
+ //@ assert valid_string(dir);
+ char *dir2 = dirname(0);
+ //@ assert valid_string(dir2);
+
+ return 0;
+}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index c1ea9b1264b8f540555594d7684ce6cc084d13d7..60e8d3f8a81faf8bef3d2ea162812f2ec0c00651 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:160: assertion got status valid.
-[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:148: assertion got status valid.
+[eva] tests/libc/fc_libc.c:149: assertion got status valid.
+[eva] tests/libc/fc_libc.c:150: assertion got status valid.
+[eva] tests/libc/fc_libc.c:151: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -37,7 +37,7 @@
wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
wmemset (0 call);
- Undefined functions (358)
+ Undefined functions (360)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_abort (1 call); Frama_C_char_interval (0 call);
@@ -69,34 +69,35 @@
alloca (0 call); asin (0 call); asinf (0 call); asinl (0 call);
at_quick_exit (0 call); atan (0 call); atan2 (0 call); atan2f (0 call);
atanf (0 call); atanl (0 call); atexit (0 call); atof (0 call);
- atol (0 call); atoll (0 call); bind (0 call); bsearch (0 call);
- bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
- clearerr (0 call); clearerr_unlocked (0 call); clock (0 call);
- clock_gettime (0 call); clock_nanosleep (0 call); close (0 call);
- closedir (0 call); closelog (0 call); connect (0 call); cos (0 call);
- cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
- difftime (0 call); div (0 call); dup (0 call); dup2 (0 call);
- execl (0 call); execle (0 call); execlp (0 call); execv (0 call);
- execve (0 call); execvp (0 call); exit (0 call); exp (0 call);
- expf (0 call); fabsl (0 call); fclose (0 call); fcntl (0 call);
- fdopen (0 call); feof (2 calls); feof_unlocked (0 call); ferror (2 calls);
- ferror_unlocked (0 call); fflush (0 call); fgetc (1 call); fgetpos (0 call);
- fgets (0 call); fgetws (0 call); fileno (0 call); fileno_unlocked (0 call);
- flock (0 call); flockfile (0 call); floor (0 call); floorf (0 call);
- floorl (0 call); fmod (0 call); fmodf (0 call); fopen (0 call);
- fork (0 call); fputc (0 call); fputs (0 call); fread (0 call);
- free (1 call); freeaddrinfo (0 call); freopen (0 call); fseek (0 call);
- fsetpos (0 call); ftell (0 call); ftrylockfile (0 call);
- funlockfile (0 call); fwrite (0 call); gai_strerror (0 call); getc (0 call);
- getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
- getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
- gethostname (0 call); getitimer (0 call); getopt (0 call);
- getopt_long (0 call); getopt_long_only (0 call); getpid (0 call);
- getppid (0 call); getpriority (0 call); getpwuid (0 call);
- getresgid (0 call); getresuid (0 call); getrlimit (0 call);
- getrusage (0 call); gets (0 call); getsid (0 call); getsockopt (0 call);
- gettimeofday (0 call); getuid (0 call); gmtime (0 call); htonl (0 call);
- htons (0 call); iconv (0 call); iconv_close (0 call); iconv_open (0 call);
+ atol (0 call); atoll (0 call); basename (0 call); bind (0 call);
+ bsearch (0 call); bzero (0 call); ceil (0 call); ceilf (0 call);
+ ceill (0 call); clearerr (0 call); clearerr_unlocked (0 call);
+ clock (0 call); clock_gettime (0 call); clock_nanosleep (0 call);
+ close (0 call); closedir (0 call); closelog (0 call); connect (0 call);
+ cos (0 call); cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
+ difftime (0 call); dirname (0 call); div (0 call); dup (0 call);
+ dup2 (0 call); execl (0 call); execle (0 call); execlp (0 call);
+ execv (0 call); execve (0 call); execvp (0 call); exit (0 call);
+ exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
+ fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
+ ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
+ fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
+ fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
+ floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
+ fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+ fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
+ freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
+ ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
+ gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
+ getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+ getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+ getitimer (0 call); getopt (0 call); getopt_long (0 call);
+ getopt_long_only (0 call); getpid (0 call); getppid (0 call);
+ getpriority (0 call); getpwuid (0 call); getresgid (0 call);
+ getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
+ getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
+ getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
+ iconv (0 call); iconv_close (0 call); iconv_open (0 call);
inet_addr (0 call); inet_ntoa (0 call); inet_ntop (0 call);
inet_pton (0 call); isascii (0 call); kill (0 call); labs (0 call);
ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
@@ -148,12 +149,12 @@
wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
wmemcmp (0 call); wmemmove (0 call); write (0 call);
- 'Extern' global variables (15)
+ 'Extern' global variables (17)
==============================
- __fc_getpwuid_pw_dir; __fc_getpwuid_pw_gid; __fc_getpwuid_pw_name;
- __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_getpwuid_pw_uid;
- __fc_hostname; __fc_mblen_state; __fc_mbtowc_state; __fc_strerror;
- __fc_wctomb_state; optarg; opterr; optopt; tzname
+ __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_gid;
+ __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell;
+ __fc_getpwuid_pw_uid; __fc_hostname; __fc_mblen_state; __fc_mbtowc_state;
+ __fc_strerror; __fc_wctomb_state; optarg; opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -163,13 +164,13 @@
==============
Sloc = 948
Decision point = 183
- Global variables = 54
+ Global variables = 58
If = 174
Loop = 40
Goto = 78
Assignment = 379
Exit point = 73
- Function = 431
+ Function = 433
Function call = 73
Pointer dereferencing = 146
Cyclomatic complexity = 256
@@ -193,6 +194,7 @@
#include "glob.h"
#include "iconv.h"
#include "inttypes.h"
+#include "libgen.h"
#include "locale.c"
#include "locale.h"
#include "math.c"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index b195276fdca49a5211a17e206797d2883d4ea43b..ca6d82677730323b0caf2c381e8440319f4a8896 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6427,6 +6427,36 @@ extern int iconv_close(iconv_t);
*/
extern iconv_t iconv_open(char const *tocode, char const *fromcode);
+extern char __fc_basename[256];
+
+char *__fc_p_basename = __fc_basename;
+/*@ requires
+ null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
+ ensures
+ result_points_to_internal_storage_or_path:
+ \subset(\result, \union(__fc_p_basename, \old(path)));
+ assigns *(path + (0 ..)), __fc_basename[0 ..], \result;
+ assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_basename[0 ..];
+ assigns __fc_basename[0 ..] \from *(path + (0 ..)), __fc_basename[0 ..];
+ assigns \result \from __fc_p_basename, path;
+ */
+extern char *basename(char *path);
+
+extern char __fc_dirname[256];
+
+char *__fc_p_dirname = __fc_dirname;
+/*@ requires
+ null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
+ ensures
+ result_points_to_internal_storage_or_path:
+ \subset(\result, \union(__fc_p_dirname, \old(path)));
+ assigns *(path + (0 ..)), __fc_dirname[0 ..], \result;
+ assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_dirname[0 ..];
+ assigns __fc_dirname[0 ..] \from *(path + (0 ..)), __fc_dirname[0 ..];
+ assigns \result \from __fc_p_dirname, path;
+ */
+extern char *dirname(char *path);
+
/*@ requires valid_file_descriptors: \valid(fds + (0 .. nfds - 1));
ensures
error_timeout_or_bounded:
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 6b9a23013e847f252018dedf4ae23366c1661de7..6650a34b1f8c6d193393997a674224079b26f14a 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -63,13 +63,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/inttypes.h (with preprocessing)
[kernel] Parsing share/libc/iso646.h (with preprocessing)
[kernel] Parsing share/libc/libgen.h (with preprocessing)
-[kernel] Parsing share/libc/libintl.h (with preprocessing)
[kernel] Parsing share/libc/limits.h (with preprocessing)
-[kernel] Parsing share/libc/linux/fs.h (with preprocessing)
-[kernel] Parsing share/libc/linux/if_addr.h (with preprocessing)
-[kernel] Parsing share/libc/linux/if_netlink.h (with preprocessing)
-[kernel] Parsing share/libc/linux/netlink.h (with preprocessing)
-[kernel] Parsing share/libc/linux/rtnetlink.h (with preprocessing)
[kernel] Parsing share/libc/locale.h (with preprocessing)
[kernel] Parsing share/libc/malloc.h (with preprocessing)
[kernel] Parsing share/libc/math.h (with preprocessing)
@@ -77,9 +71,6 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/net/if.h (with preprocessing)
[kernel] Parsing share/libc/netdb.h (with preprocessing)
[kernel] Parsing share/libc/netinet/in.h (with preprocessing)
-[kernel] Parsing share/libc/netinet/in_systm.h (with preprocessing)
-[kernel] Parsing share/libc/netinet/ip.h (with preprocessing)
-[kernel] Parsing share/libc/netinet/ip_icmp.h (with preprocessing)
[kernel] Parsing share/libc/netinet/tcp.h (with preprocessing)
[kernel] Parsing share/libc/nl_types.h (with preprocessing)
[kernel] Parsing share/libc/poll.h (with preprocessing)
@@ -104,7 +95,6 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/sys/ioctl.h (with preprocessing)
[kernel] Parsing share/libc/sys/ipc.h (with preprocessing)
[kernel] Parsing share/libc/sys/mman.h (with preprocessing)
-[kernel] Parsing share/libc/sys/param.h (with preprocessing)
[kernel] Parsing share/libc/sys/random.h (with preprocessing)
[kernel] Parsing share/libc/sys/resource.h (with preprocessing)
[kernel] Parsing share/libc/sys/select.h (with preprocessing)
@@ -112,7 +102,6 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/sys/signal.h (with preprocessing)
[kernel] Parsing share/libc/sys/socket.h (with preprocessing)
[kernel] Parsing share/libc/sys/stat.h (with preprocessing)
-[kernel] Parsing share/libc/sys/sysctl.h (with preprocessing)
[kernel] Parsing share/libc/sys/time.h (with preprocessing)
[kernel] Parsing share/libc/sys/times.h (with preprocessing)
[kernel] Parsing share/libc/sys/timex.h (with preprocessing)
@@ -125,7 +114,6 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/termios.h (with preprocessing)
skipping share/libc/tgmath.h
[kernel] Parsing share/libc/time.h (with preprocessing)
-[kernel] Parsing share/libc/uchar.h (with preprocessing)
[kernel] Parsing share/libc/unistd.h (with preprocessing)
[kernel] Parsing share/libc/utime.h (with preprocessing)
[kernel] Parsing share/libc/utmpx.h (with preprocessing)
diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ca158666adf08acb2890a53b2ae8fecfddb3e132
--- /dev/null
+++ b/tests/libc/oracle/libgen_h.res.oracle
@@ -0,0 +1,48 @@
+[kernel] Parsing tests/libc/libgen_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function basename <- main.
+ Called from tests/libc/libgen_h.c:9.
+[eva] using specification for function basename
+[eva] tests/libc/libgen_h.c:9:
+ function basename: precondition 'null_or_valid_string_path' got status valid.
+[eva] Done for function basename
+[eva:alarm] tests/libc/libgen_h.c:10: Warning: assertion got status unknown.
+[eva] computing for function basename <- main.
+ Called from tests/libc/libgen_h.c:11.
+[eva] tests/libc/libgen_h.c:11:
+ function basename: precondition 'null_or_valid_string_path' got status valid.
+[eva] tests/libc/libgen_h.c:11: Warning:
+ Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
+[eva] Done for function basename
+[eva:alarm] tests/libc/libgen_h.c:12: Warning: assertion got status unknown.
+[eva] computing for function dirname <- main.
+ Called from tests/libc/libgen_h.c:14.
+[eva] using specification for function dirname
+[eva:alarm] tests/libc/libgen_h.c:14: Warning:
+ function dirname: precondition 'null_or_valid_string_path' got status unknown.
+[eva] Done for function dirname
+[eva:alarm] tests/libc/libgen_h.c:15: Warning: assertion got status unknown.
+[eva] computing for function dirname <- main.
+ Called from tests/libc/libgen_h.c:16.
+[eva] tests/libc/libgen_h.c:16:
+ function dirname: precondition 'null_or_valid_string_path' got status valid.
+[eva] tests/libc/libgen_h.c:16: Warning:
+ Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
+[eva] Done for function dirname
+[eva:alarm] tests/libc/libgen_h.c:17: Warning: assertion got status unknown.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_basename[0..255] ∈ [--..--]
+ __fc_dirname[0..255] ∈ [--..--]
+ path[0..127] ∈ [--..--]
+ base ∈ {{ &__fc_basename[0] ; &path[0] }}
+ base2 ∈ {{ NULL ; &__fc_basename[0] }}
+ dir ∈ {{ &__fc_dirname[0] ; &path[0] }}
+ dir2 ∈ {{ NULL ; &__fc_dirname[0] }}
+ __retres ∈ {0}
diff --git a/tests/spec/clash_double_file_bts1598.c b/tests/spec/clash_double_file_bts1598.c
index 9903d9ed17ff2676f5d353e8bb04ef51a2a17898..ca549981a5bf117bea05f296554329ef7ebe4e0d 100644
--- a/tests/spec/clash_double_file_bts1598.c
+++ b/tests/spec/clash_double_file_bts1598.c
@@ -28,6 +28,5 @@ OPT: @PTEST_FILE@ -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode
#include "string.h"
//#include "tgmath.h"
#include "time.h"
-#include "uchar.h"
#include "wchar.h"
#include "wctype.h"