diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 90def1eb36789bcf7ad67f2739707038715a56ba..8edd41b725ca4d2b6daea0b05e64e1f823f9fe4d 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -251,6 +251,7 @@ 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/ip.h: CEA_LGPL
share/libc/netinet/tcp.h: CEA_LGPL
share/libc/nl_types.h: CEA_LGPL
share/libc/poll.h: CEA_LGPL
diff --git a/share/libc/__fc_integer.h b/share/libc/__fc_integer.h
index a1ae2183b3ff341163cf1a55f67103d392c9eb48..ec13533449295ac9a7109e66bc37f7e7c3b38383 100644
--- a/share/libc/__fc_integer.h
+++ b/share/libc/__fc_integer.h
@@ -25,6 +25,7 @@
#define Frama_C_INTEGER
#include "features.h"
__PUSH_FC_STDLIB
+__BEGIN_DECLS
/*@
@@ -32,5 +33,6 @@ __PUSH_FC_STDLIB
*/
+__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/netinet/ip.h b/share/libc/netinet/ip.h
new file mode 100644
index 0000000000000000000000000000000000000000..e4e709f347008b1b99daf8f5921f7e841fc443bb
--- /dev/null
+++ b/share/libc/netinet/ip.h
@@ -0,0 +1,205 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2020 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+// This is a non-POSIX file, provided for better compatibility on a
+// best-effort basis.
+
+#ifndef __NETINET_IP_H
+#define __NETINET_IP_H
+#include "../features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+#include "../__fc_inet.h"
+
+// The definitions below suppose a little endian architecture.
+
+struct timestamp
+{
+ uint8_t len;
+ uint8_t ptr;
+ unsigned int flags:4;
+ unsigned int overflow:4;
+ uint32_t data[9];
+};
+
+struct iphdr
+{
+ unsigned int ihl:4;
+ unsigned int version:4;
+ uint8_t tos;
+ uint16_t tot_len;
+ uint16_t id;
+ uint16_t frag_off;
+ uint8_t ttl;
+ uint8_t protocol;
+ uint16_t check;
+ uint32_t saddr;
+ uint32_t daddr;
+};
+
+struct ip
+{
+ unsigned int ip_hl:4;
+ unsigned int ip_v:4;
+ uint8_t ip_tos;
+ unsigned short ip_len;
+ unsigned short ip_id;
+ unsigned short ip_off;
+ uint8_t ip_ttl;
+ uint8_t ip_p;
+ unsigned short ip_sum;
+ struct in_addr ip_src, ip_dst;
+};
+
+#define IP_RF 0x8000
+#define IP_DF 0x4000
+#define IP_MF 0x2000
+#define IP_OFFMASK 0x1fff
+
+struct ip_timestamp
+{
+ uint8_t ipt_code;
+ uint8_t ipt_len;
+ uint8_t ipt_ptr;
+ unsigned int ipt_flg:4;
+ unsigned int ipt_oflw:4;
+ uint32_t data[9];
+};
+
+#define IPVERSION 4
+#define IP_MAXPACKET 65535
+
+#define IPTOS_ECN_MASK 0x03
+#define IPTOS_ECN(x) ((x) & IPTOS_ECN_MASK)
+#define IPTOS_ECN_NOT_ECT 0x00
+#define IPTOS_ECN_ECT1 0x01
+#define IPTOS_ECN_ECT0 0x02
+#define IPTOS_ECN_CE 0x03
+
+#define IPTOS_DSCP_MASK 0xfc
+#define IPTOS_DSCP(x) ((x) & IPTOS_DSCP_MASK)
+#define IPTOS_DSCP_AF11 0x28
+#define IPTOS_DSCP_AF12 0x30
+#define IPTOS_DSCP_AF13 0x38
+#define IPTOS_DSCP_AF21 0x48
+#define IPTOS_DSCP_AF22 0x50
+#define IPTOS_DSCP_AF23 0x58
+#define IPTOS_DSCP_AF31 0x68
+#define IPTOS_DSCP_AF32 0x70
+#define IPTOS_DSCP_AF33 0x78
+#define IPTOS_DSCP_AF41 0x88
+#define IPTOS_DSCP_AF42 0x90
+#define IPTOS_DSCP_AF43 0x98
+#define IPTOS_DSCP_EF 0xb8
+
+#define IPTOS_CLASS_MASK 0xe0
+#define IPTOS_CLASS(class) ((class) & IPTOS_CLASS_MASK)
+#define IPTOS_CLASS_CS0 0x00
+#define IPTOS_CLASS_CS1 0x20
+#define IPTOS_CLASS_CS2 0x40
+#define IPTOS_CLASS_CS3 0x60
+#define IPTOS_CLASS_CS4 0x80
+#define IPTOS_CLASS_CS5 0xa0
+#define IPTOS_CLASS_CS6 0xc0
+#define IPTOS_CLASS_CS7 0xe0
+
+#define IPTOS_CLASS_DEFAULT IPTOS_CLASS_CS0
+
+#define IPTOS_TOS_MASK 0x1E
+#define IPTOS_TOS(tos) ((tos) & IPTOS_TOS_MASK)
+#define IPTOS_LOWDELAY 0x10
+#define IPTOS_THROUGHPUT 0x08
+#define IPTOS_RELIABILITY 0x04
+#define IPTOS_LOWCOST 0x02
+#define IPTOS_MINCOST IPTOS_LOWCOST
+
+#define IPTOS_PREC_MASK IPTOS_CLASS_MASK
+#define IPTOS_PREC(tos) IPTOS_CLASS(tos)
+#define IPTOS_PREC_NETCONTROL IPTOS_CLASS_CS7
+#define IPTOS_PREC_INTERNETCONTROL IPTOS_CLASS_CS6
+#define IPTOS_PREC_CRITIC_ECP IPTOS_CLASS_CS5
+#define IPTOS_PREC_FLASHOVERRIDE IPTOS_CLASS_CS4
+#define IPTOS_PREC_FLASH IPTOS_CLASS_CS3
+#define IPTOS_PREC_IMMEDIATE IPTOS_CLASS_CS2
+#define IPTOS_PREC_PRIORITY IPTOS_CLASS_CS1
+#define IPTOS_PREC_ROUTINE IPTOS_CLASS_CS0
+
+#define IPOPT_COPY 0x80
+#define IPOPT_CLASS_MASK 0x60
+#define IPOPT_NUMBER_MASK 0x1f
+
+#define IPOPT_COPIED(o) ((o) & IPOPT_COPY)
+#define IPOPT_CLASS(o) ((o) & IPOPT_CLASS_MASK)
+#define IPOPT_NUMBER(o) ((o) & IPOPT_NUMBER_MASK)
+
+#define IPOPT_CONTROL 0x00
+#define IPOPT_RESERVED1 0x20
+#define IPOPT_DEBMEAS 0x40
+#define IPOPT_MEASUREMENT IPOPT_DEBMEAS
+#define IPOPT_RESERVED2 0x60
+
+#define IPOPT_EOL 0
+#define IPOPT_END IPOPT_EOL
+#define IPOPT_NOP 1
+#define IPOPT_NOOP IPOPT_NOP
+
+#define IPOPT_RR 7
+#define IPOPT_TS 68
+#define IPOPT_TIMESTAMP IPOPT_TS
+#define IPOPT_SECURITY 130
+#define IPOPT_SEC IPOPT_SECURITY
+#define IPOPT_LSRR 131
+#define IPOPT_SATID 136
+#define IPOPT_SID IPOPT_SATID
+#define IPOPT_SSRR 137
+#define IPOPT_RA 148
+
+#define IPOPT_OPTVAL 0
+#define IPOPT_OLEN 1
+#define IPOPT_OFFSET 2
+#define IPOPT_MINOFF 4
+
+#define MAX_IPOPTLEN 40
+
+#define IPOPT_TS_TSONLY 0
+#define IPOPT_TS_TSANDADDR 1
+#define IPOPT_TS_PRESPEC 3
+
+#define IPOPT_SECUR_UNCLASS 0x0000
+#define IPOPT_SECUR_CONFID 0xf135
+#define IPOPT_SECUR_EFTO 0x789a
+#define IPOPT_SECUR_MMMM 0xbc4d
+#define IPOPT_SECUR_RESTR 0xaf13
+#define IPOPT_SECUR_SECRET 0xd788
+#define IPOPT_SECUR_TOPSECRET 0x6bc5
+
+#define MAXTTL 255
+#define IPDEFTTL 64
+#define IPFRAGTTL 60
+#define IPTTLDEC 1
+
+#define IP_MSS 576
+
+__END_DECLS
+__POP_FC_STDLIB
+
+#endif
diff --git a/share/libc/netinet/tcp.h b/share/libc/netinet/tcp.h
index e6b54e6bb39df74c0e11ca3793cd46cd29abb49e..a87954a655ae87e5e60a0a79418a90b68854f658 100644
--- a/share/libc/netinet/tcp.h
+++ b/share/libc/netinet/tcp.h
@@ -56,6 +56,7 @@
#include <features.h>
__PUSH_FC_STDLIB
+__BEGIN_DECLS
/*
* User-settable options (used with setsockopt).
@@ -342,6 +343,7 @@ struct tcp_cookie_transactions
#endif /* Misc. */
+__END_DECLS
__POP_FC_STDLIB
#endif /* netinet/tcp.h */
diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index 1d1e8fd806abf584768b36de2d2ebf5a4a0acf35..cb5f7f538a9213bbca5092d962708c6c5f72fd3c 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -25,6 +25,7 @@
#include "features.h"
__PUSH_FC_STDLIB
+__BEGIN_DECLS
#include "errno.h"
@@ -369,5 +370,6 @@ extern void pthread_testcancel(void);
// (sched.h has already been included)
#include "time.h"
+__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/file.h b/share/libc/sys/file.h
index 6744af37fc860cbc478c4b31c8ecf3ca883b23e8..b627e24badd85e725310daaa6287a44af726f248 100644
--- a/share/libc/sys/file.h
+++ b/share/libc/sys/file.h
@@ -25,6 +25,7 @@
#include "../features.h"
__PUSH_FC_STDLIB
+__BEGIN_DECLS
// Note: this file is not C11 nor POSIX, but Linux-specific.
// The values for the constants below are based on the glibc.
@@ -46,5 +47,6 @@ __PUSH_FC_STDLIB
*/
extern int flock(int fd, int operation);
+__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/mman.h b/share/libc/sys/mman.h
index 9bc0105c71feebb46e6c5c3354e497d3d90a3c47..ed2baf1ff2c81de8c8870e24bd878b21d4cf5ab8 100644
--- a/share/libc/sys/mman.h
+++ b/share/libc/sys/mman.h
@@ -28,6 +28,7 @@
#include "../__fc_define_off_t.h"
#include "../__fc_define_size_t.h"
__PUSH_FC_STDLIB
+__BEGIN_DECLS
// The values for the constants below are based on an x86 Linux,
// declared in the order given by POSIX.1-2008.
@@ -92,5 +93,6 @@ extern int posix_madvise (void *__addr, size_t __len, int __advice);
extern int shm_open (const char *__name, int __oflag, mode_t __mode);
extern int shm_unlink (const char *__name);
+__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/times.h b/share/libc/sys/times.h
index 8ec99d000d9cfa84bf00d3302d9d2810bd069f08..8d54e4e2edaa7f894ec571f4575070beb2c8525d 100644
--- a/share/libc/sys/times.h
+++ b/share/libc/sys/times.h
@@ -25,6 +25,7 @@
#include "../features.h"
__PUSH_FC_STDLIB
+__BEGIN_DECLS
#include "../time.h"
struct tms
@@ -38,5 +39,7 @@ struct tms
/*@ requires valid_buffer: \valid(buffer);
assigns \result, *buffer \from __fc_time; */
extern clock_t times (struct tms *buffer);
+
+__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/utsname.h b/share/libc/sys/utsname.h
index e60cacea8b185e8452c44e948a147ce6348c5556..b26453462934619f6359b93963bc0b95e13bda93 100644
--- a/share/libc/sys/utsname.h
+++ b/share/libc/sys/utsname.h
@@ -25,6 +25,7 @@
#include "../features.h"
__PUSH_FC_STDLIB
+__BEGIN_DECLS
// Arbitrary length, based on the one used in Linux
#define _FC_UTSNAME_LENGTH 65
@@ -46,5 +47,6 @@ struct utsname
*/
extern int uname (struct utsname *name);
+__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index db68bcf3adf8d06663093e725347cb4f8ae7de7f..5ad226916ca36cd0496df4992e45e78d79a22da2 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -98,6 +98,7 @@
#include "netdb.h"
#include "net/if.h"
#include "netinet/in.h"
+#include "netinet/ip.h"
#include "netinet/tcp.h"
#include "nl_types.h"
#include "poll.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index d0a318762b25eed2f4bbcf4f604f864e49adb936..e3ca27e4863a5c853bf6c387842e38e4363e8e51 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:154: assertion got status valid.
[eva] tests/libc/fc_libc.c:155: assertion got status valid.
[eva] tests/libc/fc_libc.c:156: assertion got status valid.
[eva] tests/libc/fc_libc.c:157: assertion got status valid.
+[eva] tests/libc/fc_libc.c:158: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 4b7f321bdaefa863bb3a434a0f0479af8319120d..b1e1247a43669f03d504de710fa2a4b5337ce754 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -73,6 +73,7 @@ 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/ip.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)