diff --git a/share/libc/byteswap.h b/share/libc/byteswap.h
index f3ca11ff17c469366fa7ef95ee99d9c21d921efd..37cea739c8b27a5fa4a2b79f0f501ca46b00e7cd 100644
--- a/share/libc/byteswap.h
+++ b/share/libc/byteswap.h
@@ -80,7 +80,7 @@
# define __bswap_64(x) \
(__extension__ \
- ({ union { __extension__ unsigned long long int __ll; \
+ ({ union __fc_bswap { __extension__ unsigned long long int __ll; \
unsigned int __l[2]; } __w, __r; \
if (__builtin_constant_p (x)) \
__r.__ll = __bswap_constant_64 (x); \
diff --git a/share/libc/dirent.h b/share/libc/dirent.h
index 6d75102f9e1bb1e51ca609e8d532fdfdda787cd0..df5d82212c54b97b81a82f61086b8e3cbf6a867c 100644
--- a/share/libc/dirent.h
+++ b/share/libc/dirent.h
@@ -99,7 +99,7 @@ extern long telldir(DIR *);
/* File types for `d_type'. */
-enum
+enum __fc_readdir_dtype
{
DT_UNKNOWN = 0,
# define DT_UNKNOWN DT_UNKNOWN
diff --git a/share/libc/ifaddrs.h b/share/libc/ifaddrs.h
index 9c1cadd191bf1f357ca9e077694639d9cdd03ef7..b66ab2e939e82808d228461181d0c6fbca933d80 100644
--- a/share/libc/ifaddrs.h
+++ b/share/libc/ifaddrs.h
@@ -37,7 +37,7 @@ struct ifaddrs {
struct sockaddr *ifa_addr;
struct sockaddr *ifa_netmask;
struct sockaddr *ifa_dstaddr;
- union {
+ union __fc_ifaddrs_ifa_ifu {
struct sockaddr *ifu_broadaddr;
struct sockaddr *ifu_dstaddr;
} ifa_ifu;
diff --git a/share/libc/net/if.h b/share/libc/net/if.h
index 0b92ebd79829f463d0370a2b5ef0056eeb660e0b..5fac010b5d8af754758405404ed876b4dfff14bd 100644
--- a/share/libc/net/if.h
+++ b/share/libc/net/if.h
@@ -71,7 +71,7 @@ extern void if_freenameindex(struct if_nameindex *ni);
struct ifaddr
{
struct sockaddr ifa_addr; /* Address of interface. */
- union
+ union __fc_ifa_ifu
{
struct sockaddr ifu_broadaddr;
struct sockaddr ifu_dstaddr;
@@ -111,11 +111,11 @@ struct ifmap {
struct ifreq {
# define IFHWADDRLEN 6
# define IFNAMSIZ IF_NAMESIZE
- union {
+ union __fc_ifr_ifrn {
char ifrn_name[IFNAMSIZ]; /* Interface name, e.g. "en0". */
} ifr_ifrn;
- union {
+ union __fc_ifr_ifru {
struct sockaddr ifru_addr;
struct sockaddr ifru_dstaddr;
struct sockaddr ifru_broadaddr;
@@ -154,7 +154,7 @@ struct ifreq {
struct ifconf
{
int ifc_len; /* Size of buffer. */
- union
+ union __fc_ifc_ifcu
{
char *ifcu_buf;
struct ifreq *ifcu_req;
diff --git a/share/libc/netinet/tcp.h b/share/libc/netinet/tcp.h
index fb7abe05a65782a53e85991a95ebfab6b4c479ee..a1abf7157f3e83f9c3e1610981bbb2ddbb169f19 100644
--- a/share/libc/netinet/tcp.h
+++ b/share/libc/netinet/tcp.h
@@ -115,9 +115,9 @@ typedef u_int32_t tcp_seq;
*/
struct tcphdr
{
- __extension__ union
+ __extension__ union __fc_tcphdr
{
- struct
+ struct __fc_tcp_header_1
{
u_int16_t th_sport; /* source port */
u_int16_t th_dport; /* destination port */
@@ -142,7 +142,7 @@ struct tcphdr
u_int16_t th_sum; /* checksum */
u_int16_t th_urp; /* urgent pointer */
};
- struct
+ struct __fc_tcp_header_2
{
u_int16_t source;
u_int16_t dest;
@@ -178,7 +178,7 @@ struct tcphdr
};
};
-enum
+enum __fc_tcp_state
{
TCP_ESTABLISHED = 1,
TCP_SYN_SENT,
@@ -305,7 +305,7 @@ struct tcp_repair_opt
};
/* Queue to repair, for TCP_REPAIR_QUEUE. */
-enum
+enum __fc_tcp_queue
{
TCP_NO_QUEUE,
TCP_RECV_QUEUE,
diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index ac9f78bc234e099c4e77ec0690697b2173030e18..eb5a186e082560b4a3564580ae3469cbe7f3d9ae 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -31,25 +31,25 @@ __PUSH_FC_STDLIB
// The values for the constants below are based on an x86 Linux,
// declared in the order given by POSIX.1-2008.
-enum
+enum __fc_pthread_cancelstate
{
PTHREAD_CANCEL_ENABLE,
PTHREAD_CANCEL_DISABLE
};
-enum
+enum __fc_pthread_canceltype
{
PTHREAD_CANCEL_DEFERRED,
PTHREAD_CANCEL_ASYNCHRONOUS
};
-enum
+enum __fc_pthread_detachstate
{
PTHREAD_CREATE_JOINABLE,
PTHREAD_CREATE_DETACHED
};
-enum
+enum __fc_pthread_inheritsched
{
PTHREAD_INHERIT_SCHED,
PTHREAD_EXPLICIT_SCHED
@@ -57,13 +57,13 @@ enum
/* Scope handling. */
-enum
+enum __fc_pthread_scope
{
PTHREAD_SCOPE_SYSTEM,
PTHREAD_SCOPE_PROCESS
};
-enum
+enum __fc_pthread_mutex_type
{
PTHREAD_MUTEX_NORMAL,
PTHREAD_MUTEX_RECURSIVE,
@@ -71,20 +71,20 @@ enum
PTHREAD_MUTEX_DEFAULT
};
-enum
+enum __fc_pthread_mutex_robust
{
PTHREAD_MUTEX_STALLED,
PTHREAD_MUTEX_ROBUST
};
-enum
+enum __fc_pthread_mutex_protocol
{
PTHREAD_PRIO_NONE,
PTHREAD_PRIO_INHERIT,
PTHREAD_PRIO_PROTECT
};
-enum
+enum __fc_pthread_mutex_pshared
{
PTHREAD_PROCESS_PRIVATE,
PTHREAD_PROCESS_SHARED
diff --git a/share/libc/semaphore.h b/share/libc/semaphore.h
index 765cd52cb54e180d73188d19c4973ee4b3eb615d..dc25bc5309169e5e3a7a4b3e5ea48ff4ef76cb27 100644
--- a/share/libc/semaphore.h
+++ b/share/libc/semaphore.h
@@ -30,7 +30,7 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-typedef union {
+typedef union __fc_sem_t {
char __size[16];
} sem_t;
diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index c8d2a9ae4c3ce84d3762610595f048d30339c701..eb57e0efbaa5ee79c9810fe091b10d253e9c868d 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -269,7 +269,7 @@ extern unsigned char *CMSG_DATA(struct cmsghdr *cmsg);
#define SOMAXCONN 128
-enum {
+enum __fc_shutdown {
SHUT_RD,
SHUT_WR,
SHUT_RDWR
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index e0c2a6817d3815b62976ad186b17f3947b859aec..4a8a0455ceb36a581255d0a30a29e4f94a198aba 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -68,7 +68,7 @@ extern volatile int Frama_C_entropy_source;
__BEGIN_DECLS
/* Values for the NAME argument to `pathconf' and `fpathconf'. */
-enum
+enum __fc_pathconf_name
{
_PC_LINK_MAX,
#define _PC_LINK_MAX _PC_LINK_MAX
@@ -115,7 +115,7 @@ enum
};
/* Values for the argument to `sysconf'. */
-enum
+enum __fc_sysconf_name
{
_SC_ARG_MAX,
#define _SC_ARG_MAX _SC_ARG_MAX
@@ -577,7 +577,7 @@ enum
};
/* Values for the NAME argument to `confstr'. */
-enum
+enum __fc_confstr_name
{
_CS_PATH, /* The default search path. */
#define _CS_PATH _CS_PATH
diff --git a/tests/libc/check_libc_anonymous_tags.ml b/tests/libc/check_libc_anonymous_tags.ml
new file mode 100644
index 0000000000000000000000000000000000000000..62bb754fb908f86bb3bbb7bdb0fc903341eb20f4
--- /dev/null
+++ b/tests/libc/check_libc_anonymous_tags.ml
@@ -0,0 +1,57 @@
+(* Checks that the Frama-C libc does not declare any anonymous
+ enums/structs/unions *)
+
+open Cil_types
+
+class tags_visitor = object
+ inherit Visitor.frama_c_inplace
+ val in_stdlib = ref false
+
+ method! vglob_aux g =
+ if Cil.hasAttribute "fc_stdlib" (Cil.global_attributes g) then
+ begin
+ in_stdlib := true;
+ begin
+ match g with
+ | GEnumTag (ei, loc) | GEnumTagDecl (ei, loc) ->
+ if ei.eorig_name = "" && !in_stdlib then
+ Kernel.warning ~source:(fst loc) ~once:true
+ "anonymous enum in Frama-C stdlib";
+ | GCompTag (ci, loc) | GCompTagDecl (ci, loc) ->
+ if ci.corig_name = "" && !in_stdlib then
+ Kernel.warning ~source:(fst loc) ~once:true
+ "anonymous %s in Frama-C stdlib"
+ (if ci.cstruct then "struct" else "union");
+ | _ -> ()
+ end;
+ Cil.DoChildren
+ end
+ else begin
+ in_stdlib := false;
+ Cil.SkipChildren
+ end
+
+ method! vtype typ =
+ begin
+ match typ with
+ | TEnum (ei, _) when ei.eorig_name = "" && !in_stdlib ->
+ Kernel.warning ~current:true ~once:true
+ "anonymous enum in Frama-C stdlib";
+ ()
+ | TComp (ci, _, _) when ci.corig_name = "" && !in_stdlib ->
+ Kernel.warning ~current:true ~once:true
+ "anonymous %s in Frama-C stdlib"
+ (if ci.cstruct then "struct" else "union")
+ | _ -> ()
+ end;
+ Cil.DoChildren
+end
+
+let run_once = ref false
+
+let () =
+ Db.Main.extend (fun () ->
+ if not !run_once then begin
+ run_once := true;
+ Visitor.visitFramacFile (new tags_visitor) (Ast.get ())
+ end)
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 108fa7a3ad4a0cdf546d0127c2aec388f32077ae..fc52ca5ff0ad17a4190b6bb394a20cd090e22d0f 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -2,10 +2,12 @@
EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs
EXECNOW: make -s @PTEST_DIR@/check_const.cmxs
EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs
+ EXECNOW: make -s @PTEST_DIR@/check_libc_anonymous_tags.cmxs
EXECNOW: make -s @PTEST_DIR@/check_compliance.cmxs
OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
OPT: -print -print-libc
OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers
+ OPT: -load-module @PTEST_DIR@/check_libc_anonymous_tags
OPT: -load-module @PTEST_DIR@/check_compliance -kernel-msg-key printer:attrs
CMD: ./tests/libc/check_full_libc.sh
OPT:
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 7edeeaacb72c89e076fde32302ba704b09368783..d64ea807afda96b59b16bcca76633b124b9864dc 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:151: assertion got status valid.
-[eva] tests/libc/fc_libc.c:152: assertion got status valid.
[eva] tests/libc/fc_libc.c:153: assertion got status valid.
[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] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/fc_libc.3.res.oracle b/tests/libc/oracle/fc_libc.3.res.oracle
index 5d4b6982df1e929a36eb1f4f623ad3ca169e8c76..1653140b9190a1d8e1b6e75b8a21068409c46e43 100644
--- a/tests/libc/oracle/fc_libc.3.res.oracle
+++ b/tests/libc/oracle/fc_libc.3.res.oracle
@@ -1,5 +1 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
-[kernel] parsing c11_functions.json
-[kernel] parsing glibc_functions.json
-[kernel] parsing posix_identifiers.json
-[kernel] parsing nonstandard_identifiers.json
diff --git a/tests/libc/oracle/fc_libc.4.res.oracle b/tests/libc/oracle/fc_libc.4.res.oracle
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..5d4b6982df1e929a36eb1f4f623ad3ca169e8c76 100644
--- a/tests/libc/oracle/fc_libc.4.res.oracle
+++ b/tests/libc/oracle/fc_libc.4.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
+[kernel] parsing c11_functions.json
+[kernel] parsing glibc_functions.json
+[kernel] parsing posix_identifiers.json
+[kernel] parsing nonstandard_identifiers.json
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391