From 7836d10a5276e4f0997c2d8367fe8043fc6c5e8b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 23 Feb 2022 14:07:50 +0100
Subject: [PATCH] [compliance] add comments and references to hard-coded type
list of GCC builtins
---
share/compliance/gcc_builtins.json | 2 +-
src/kernel_services/ast_queries/cil_builtins.ml | 10 +++++++++-
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/share/compliance/gcc_builtins.json b/share/compliance/gcc_builtins.json
index d5cf906f7ff..860027309d2 100644
--- a/share/compliance/gcc_builtins.json
+++ b/share/compliance/gcc_builtins.json
@@ -3,7 +3,7 @@
"source":"Mostly https://gcc.gnu.org/onlinedocs/gcc/C-Extensions.html, from pages with 'Builtins' in their title",
"notes": {
"rettype":"Return type of the builtin. Whitespace is important: types are matched as exact strings, with a single space between components.",
- "args":"List of the types of the builtin arguments. Whitespace is important: types are matched as exact strings, with a single space between components.",
+ "args":"List of the types of the builtin arguments. Whitespace is important: types are matched as exact strings, with a single space between components. The full list of 'known' type names is available in cil_builtins.ml.",
"types":"When present, a list indicating that this is a builtin template, to be instantiated for each type in the list. Instantiation is the replacement of each occurrence of 'type' in 'rettype' and 'args' with the elements of this list.",
"variadic":"When present, this builtin behaves as a variadic function."
},
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 4d2aaaecf5e..76fbb26e894 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -241,7 +241,12 @@ end
(* For performance, this table provides O(1) lookups between type names
and the underlying Cil types. Some types may be unavailable in some
- machdeps, so the table returns an option type. *)
+ machdeps, so the table returns an option type.
+ Note that the type strings must follow a strict format (also used
+ in gcc_builtins.json), with a single space between type names and
+ asterisks (for pointers); otherwise we would have to do some expensive
+ matching.
+*)
let build_type_table () : (string, typ option) Hashtbl.t =
let int8_t = Some Cil.scharType in
let int16_t = try Some (Cil.int16_t ()) with Not_found -> None in
@@ -317,6 +322,9 @@ let build_type_table () : (string, typ option) Hashtbl.t =
] in
Hashtbl.of_seq (List.to_seq types)
+(* Note that [s] (the type string) follows a stricter format than the ones
+ allowed by the C standard w.r.t. type names; a single space must be
+ present between type names and asterisks. *)
let parse_type ?(template="") type_table s =
try
if String.get s 0 == 'T' then
--
GitLab