diff --git a/share/compliance/gcc_builtins.json b/share/compliance/gcc_builtins.json
index d5cf906f7ffb4f0131d2925864dfa18332ac624c..860027309d28c5c7e83d0b5b1a0483ae1b4ecc21 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 4d2aaaecf5e4120ab32054cfd105a6ccc5a0b550..76fbb26e89423910b4331e8961f1d717c80f9899 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