From 27d8c48f0c626c7a351ec25691ff01b66477e2bb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 16 Oct 2020 14:31:14 +0200
Subject: [PATCH] [Compliance] add C11 headers
---
share/compliance/c11_headers.json | 35 ++++++++++++++++++++++++++
tests/libc/check_compliance.ml | 20 ++++++++-------
tests/libc/oracle/fc_libc.4.res.oracle | 1 +
3 files changed, 47 insertions(+), 9 deletions(-)
create mode 100644 share/compliance/c11_headers.json
diff --git a/share/compliance/c11_headers.json b/share/compliance/c11_headers.json
new file mode 100644
index 00000000000..82f65fafa3b
--- /dev/null
+++ b/share/compliance/c11_headers.json
@@ -0,0 +1,35 @@
+{
+ "description": "C11 standard library headers",
+ "source":"ISO/IEC 9899:2011, 7.1.2§2",
+ "data":[
+ "assert.h",
+ "complex.h",
+ "ctype.h",
+ "errno.h",
+ "fenv.h",
+ "float.h",
+ "inttypes.h",
+ "iso646.h",
+ "limits.h",
+ "locale.h",
+ "math.h",
+ "setjmp.h",
+ "signal.h",
+ "stdalign.h",
+ "stdarg.h",
+ "stdatomic.h",
+ "stdbool.h",
+ "stddef.h",
+ "stdint.h",
+ "stdio.h",
+ "stdlib.h",
+ "stdnoreturn.h",
+ "string.h",
+ "tgmath.h",
+ "threads.h",
+ "time.h",
+ "uchar.h",
+ "wchar.h",
+ "wctype.h"
+ ]
+}
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index a9d5043ecad..2f557ed0ec1 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -45,7 +45,7 @@ let run_once = ref false
module StringSet = Set.Make(String)
-let get_idents_from_list dir f =
+let set_of_data_from_list dir f =
let file = Filename.concat dir f in
let open Yojson.Basic.Util in
Kernel.feedback "parsing %s" f;
@@ -56,7 +56,7 @@ let get_idents_from_list dir f =
) StringSet.empty elements
-let get_idents_from_assoc dir f =
+let set_of_data_from_assoc dir f =
let file = Filename.concat dir f in
let open Yojson.Basic.Util in
Kernel.feedback "parsing %s" f;
@@ -66,7 +66,7 @@ let get_idents_from_assoc dir f =
StringSet.add ident acc
) StringSet.empty elements
-let get_ident_headers dir f =
+let hashtable_of_ident_headers dir f =
let file = Filename.concat dir f in
let idents = Hashtbl.create 500 in
let open Yojson.Basic.Util in
@@ -79,7 +79,7 @@ let get_ident_headers dir f =
) elements;
idents
-let get_ident_headers_and_extensions dir f =
+let hashtable_of_ident_headers_and_extensions dir f =
let file = Filename.concat dir f in
let idents = Hashtbl.create 500 in
let open Yojson.Basic.Util in
@@ -101,10 +101,11 @@ let () =
ignore (Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ()));
let fc_stdlib_idents = vis#get_idents in
let dir = Filename.concat Fc_config.datadir "compliance" in
- let c11_idents = get_ident_headers dir "c11_functions.json" in
- let glibc_idents = get_idents_from_list dir "glibc_functions.json" in
- let posix_idents = get_ident_headers_and_extensions dir "posix_identifiers.json" in
- let nonstandard_idents = get_idents_from_assoc dir "nonstandard_identifiers.json" in
+ let c11_idents = hashtable_of_ident_headers dir "c11_functions.json" in
+ let c11_headers = set_of_data_from_list dir "c11_headers.json" in
+ let glibc_idents = set_of_data_from_list dir "glibc_functions.json" in
+ let posix_idents = hashtable_of_ident_headers_and_extensions dir "posix_identifiers.json" in
+ let nonstandard_idents = set_of_data_from_assoc dir "nonstandard_identifiers.json" in
Hashtbl.iter (fun id headers ->
if not (Extlib.string_prefix "__" id) &&
not (Extlib.string_prefix "Frama_C" id) &&
@@ -115,13 +116,14 @@ let () =
let id_in_posix = Hashtbl.mem posix_idents id in
let id_in_glibc = StringSet.mem id glibc_idents in
let id_in_nonstd = StringSet.mem id nonstandard_idents in
+ let header_in_c11 h = StringSet.mem h c11_headers in
if id_in_c11 then begin
(* Check that the header is the expected one.
Note that some symbols may appear in more than one header,
possibly due to collisions
(e.g. 'flock' as type and function). *)
let h = Hashtbl.find c11_idents id in
- if not (List.mem h headers) then
+ if not (header_in_c11 h) then
Kernel.warning "<%a>:%s : C11 says %s"
(Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
id h
diff --git a/tests/libc/oracle/fc_libc.4.res.oracle b/tests/libc/oracle/fc_libc.4.res.oracle
index 5d4b6982df1..c3d203e2697 100644
--- a/tests/libc/oracle/fc_libc.4.res.oracle
+++ b/tests/libc/oracle/fc_libc.4.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
[kernel] parsing c11_functions.json
+[kernel] parsing c11_headers.json
[kernel] parsing glibc_functions.json
[kernel] parsing posix_identifiers.json
[kernel] parsing nonstandard_identifiers.json
--
GitLab