From e865f7294a7a8e95f045feea9f3d4d850f5d1f6c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 16 Oct 2020 11:39:46 +0200
Subject: [PATCH] [Compliance] add Frama-C support level for POSIX headers
---
share/compliance/posix_identifiers.json | 171 ++++++++++++------------
1 file changed, 86 insertions(+), 85 deletions(-)
diff --git a/share/compliance/posix_identifiers.json b/share/compliance/posix_identifiers.json
index 79ff0854712..665b56480ac 100644
--- a/share/compliance/posix_identifiers.json
+++ b/share/compliance/posix_identifiers.json
@@ -2,7 +2,8 @@
"description": "POSIX.1-2008 reserved function identifiers (plus a few legacy POSIX identifiers)",
"source":"POSIX.1-2008 - Base Specifications, Issue 7 (IEEE Std 1003.1-2008, 2016 Edition)",
"notes": {
- "description": "The 'notes' field is a list of characteristics related to CWEs or that may affect the 'difficulty' of analyzing such functions with Frama-C. Each note is succintly described below.",
+ "description": "The 'notes' field is a list of characteristics related to CWEs or that may affect the 'difficulty' of analyzing such headers or functions with Frama-C. Each note is succintly described below.",
+ "fc-support":"How well Frama-C supports this construct, w.r.t. the C11 standard: 'unsupported', 'none', 'partial', or 'good'. The difference between 'unsupported' and 'none' is that the former means something requiring substantial changes to be supported by Frama-C, while the latter only means 'not tried yet'.",
"variadic-plugin":"This is a variadic function known by the Variadic plug-in, which can (in some cases) generate a specification for it."
},
"id_types":[
@@ -13,90 +14,90 @@
{"type":"constant", "description":"symbolic constant"},
{"type":"type", "description":"type or structure"}
],
- "headers":[
- "aio.h",
- "arpa/inet.h",
- "assert.h",
- "complex.h",
- "cpio.h",
- "ctype.h",
- "dirent.h",
- "dlfcn.h",
- "errno.h",
- "fcntl.h",
- "fenv.h",
- "float.h",
- "fmtmsg.h",
- "fnmatch.h",
- "ftw.h",
- "glob.h",
- "grp.h",
- "iconv.h",
- "inttypes.h",
- "iso646.h",
- "langinfo.h",
- "libgen.h",
- "limits.h",
- "locale.h",
- "math.h",
- "monetary.h",
- "mqueue.h",
- "ndbm.h",
- "net/if.h",
- "netdb.h",
- "netinet/in.h",
- "netinet/tcp.h",
- "nl_types.h",
- "poll.h",
- "pthread.h",
- "pwd.h",
- "regex.h",
- "sched.h",
- "search.h",
- "semaphore.h",
- "setjmp.h",
- "signal.h",
- "spawn.h",
- "stdarg.h",
- "stdbool.h",
- "stddef.h",
- "stdint.h",
- "stdio.h",
- "stdlib.h",
- "string.h",
- "strings.h",
- "stropts.h",
- "sys/ipc.h",
- "sys/mman.h",
- "sys/msg.h",
- "sys/resource.h",
- "sys/select.h",
- "sys/sem.h",
- "sys/shm.h",
- "sys/socket.h",
- "sys/stat.h",
- "sys/statvfs.h",
- "sys/time.h",
- "sys/times.h",
- "sys/types.h",
- "sys/uio.h",
- "sys/un.h",
- "sys/utsname.h",
- "sys/wait.h",
- "syslog.h",
- "tar.h",
- "termios.h",
- "tgmath.h",
- "time.h",
- "trace.h",
- "ulimit.h",
- "unistd.h",
- "utime.h",
- "utmpx.h",
- "wchar.h",
- "wctype.h",
- "wordexp.h"
- ],
+ "headers":{
+ "aio.h": {"fc-support":"none"},
+ "arpa/inet.h": {"fc-support":"partial"},
+ "assert.h": {"fc-support":"good"},
+ "complex.h": {"fc-support":"unsupported"},
+ "cpio.h": {"fc-support":"none"},
+ "ctype.h": {"fc-support":"good"},
+ "dirent.h": {"fc-support":"partial"},
+ "dlfcn.h": {"fc-support":"partial"},
+ "errno.h": {"fc-support":"good"},
+ "fcntl.h": {"fc-support":"partial"},
+ "fenv.h": {"fc-support":"partial"},
+ "float.h": {"fc-support":"partial"},
+ "fmtmsg.h": {"fc-support":"none"},
+ "fnmatch.h": {"fc-support":"partial"},
+ "ftw.h": {"fc-support":"partial"},
+ "glob.h": {"fc-support":"partial"},
+ "grp.h": {"fc-support":"partial"},
+ "iconv.h": {"fc-support":"partial"},
+ "inttypes.h": {"fc-support":"good"},
+ "iso646.h": {"fc-support":"good"},
+ "langinfo.h": {"fc-support":"none"},
+ "libgen.h": {"fc-support":"good"},
+ "limits.h": {"fc-support":"good"},
+ "locale.h": {"fc-support":"partial"},
+ "math.h": {"fc-support":"partial"},
+ "monetary.h": {"fc-support":"none"},
+ "mqueue.h": {"fc-support":"none"},
+ "ndbm.h": {"fc-support":"none"},
+ "net/if.h": {"fc-support":"partial"},
+ "netdb.h": {"fc-support":"partial"},
+ "netinet/in.h": {"fc-support":"partial"},
+ "netinet/tcp.h": {"fc-support":"good"},
+ "nl_types.h": {"fc-support":"partial"},
+ "poll.h": {"fc-support":"good"},
+ "pthread.h": {"fc-support":"partial"},
+ "pwd.h": {"fc-support":"partial"},
+ "regex.h": {"fc-support":"partial"},
+ "sched.h": {"fc-support":"partial"},
+ "search.h": {"fc-support":"none"},
+ "semaphore.h": {"fc-support":"partial"},
+ "setjmp.h": {"fc-support":"partial"},
+ "signal.h": {"fc-support":"partial"},
+ "spawn.h": {"fc-support":"none"},
+ "stdarg.h": {"fc-support":"good"},
+ "stdbool.h": {"fc-support":"good"},
+ "stddef.h": {"fc-support":"good"},
+ "stdint.h": {"fc-support":"good"},
+ "stdio.h": {"fc-support":"good"},
+ "stdlib.h": {"fc-support":"good"},
+ "string.h": {"fc-support":"good"},
+ "strings.h": {"fc-support":"partial"},
+ "stropts.h": {"fc-support":"partial"},
+ "sys/ipc.h": {"fc-support":"partial"},
+ "sys/mman.h": {"fc-support":"partial"},
+ "sys/msg.h": {"fc-support":"none"},
+ "sys/resource.h": {"fc-support":"good"},
+ "sys/select.h": {"fc-support":"partial"},
+ "sys/sem.h": {"fc-support":"none"},
+ "sys/shm.h": {"fc-support":"partial"},
+ "sys/socket.h": {"fc-support":"partial"},
+ "sys/stat.h": {"fc-support":"partial"},
+ "sys/statvfs.h": {"fc-support":"none"},
+ "sys/time.h": {"fc-support":"partial"},
+ "sys/times.h": {"fc-support":"partial"},
+ "sys/types.h": {"fc-support":"good"},
+ "sys/uio.h": {"fc-support":"partial"},
+ "sys/un.h": {"fc-support":"partial"},
+ "sys/utsname.h": {"fc-support":"partial"},
+ "sys/wait.h": {"fc-support":"partial"},
+ "syslog.h": {"fc-support":"partial"},
+ "tar.h": {"fc-support":"none"},
+ "termios.h": {"fc-support":"partial"},
+ "tgmath.h": {"fc-support":"unsupported"},
+ "time.h": {"fc-support":"partial"},
+ "trace.h": {"fc-support":"none"},
+ "ulimit.h": {"fc-support":"none"},
+ "unistd.h": {"fc-support":"partial"},
+ "utime.h": {"fc-support":"partial"},
+ "utmpx.h": {"fc-support":"partial"},
+ "wchar.h": {"fc-support":"partial"},
+ "wctype.h": {"fc-support":"partial"},
+ "wordexp.h": {"fc-support":"none"}
+ },
"extension_names":{
"ADV":"Advisory Information",
"CX":"Extension to the ISO C standard",
--
GitLab