[kernel] move comment about gcc builtins to JSON file and add comment on types

share/compliance/compiler_builtins.json

@@ -4,7 +4,8 @@
         "compiler":"When present, indicates this builtin is only available in Frama-C machdeps with this compiler. Allowed values: msvc, !msvc (the latter meaning: 'available in machdeps with compilers other than MSVC').",
         "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.",
-        "variadic":"When present, this builtin behaves as a variadic function."
+        "variadic":"When present, this builtin behaves as a variadic function.",
+        "_comment": "Adding new types to fields 'rettype' or 'args' requires updating the list of recognized types in 'src/kernel_services/ast_queries/cil_builtins.ml'."
     },
     "data":{
         "__builtin__annotation": {

share/compliance/gcc_builtins.json

@@ -5,7 +5,91 @@
         "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. 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."
+        "variadic":"When present, this builtin behaves as a variadic function.",
+        "_comment": [
+            "Complex types are unsupported, so the following builtins cannot be added:",
+            "cabs",
+            "cabsf",
+            "cabsh",
+            "cacos",
+            "cacosf",
+            "cacosl",
+            "cacosh",
+            "cacoshf",
+            "cacoshl",
+            "carg",
+            "cargf",
+            "cargl",
+            "casin",
+            "casinf",
+            "casinl",
+            "casinh",
+            "casinhf",
+            "casinhl",
+            "catan",
+            "catanf",
+            "catanl",
+            "catanh",
+            "catanhf",
+            "catanhl",
+            "ccos",
+            "ccosf",
+            "ccosl",
+            "ccosh",
+            "ccoshf",
+            "ccoshl",
+            "cexp",
+            "cexpf",
+            "cexpl",
+            "cimag",
+            "cimagf",
+            "cimagl",
+            "clog",
+            "clogf",
+            "clogl",
+            "conj",
+            "conjf",
+            "conjl",
+            "cpow",
+            "cpowf",
+            "cpowl",
+            "cproj",
+            "cprojf",
+            "cprojl",
+            "creal",
+            "crealf",
+            "creall",
+            "csin",
+            "csinf",
+            "csinl",
+            "csinh",
+            "csinhf",
+            "csinhl",
+            "csqrt",
+            "csqrtf",
+            "csqrtl",
+            "ctan",
+            "ctanf",
+            "ctanl",
+            "ctanh",
+            "ctanhf",
+            "ctanhl",
+            "Also, the type 'wint_t' is not specified in 'theMachine', so the following builtins that use it cannot be added:",
+            "iswalnum",
+            "iswalpha",
+            "iswblank",
+            "iswcntrl",
+            "iswdigit",
+            "iswgraph",
+            "iswlower",
+            "iswprint",
+            "iswpunct",
+            "iswspace",
+            "iswupper",
+            "iswxdigit",
+            "towlower",
+            "towupper"
+        ]
     },
     "data":{
         "__builtin__Exit": {

src/kernel_services/ast_queries/cil_builtins.ml

@@ -344,43 +344,6 @@ let is_machdep_active compiler =
   | Some Not_MSVC, _, false -> true
   | _, _, _ -> false
 
-(* Complex types are unsupported so the following built-ins can't be added :
-   - cabs, cabsf, cabsh
-   - cacos, cacosf, cacosl, cacosh, cacoshf, cacoshl
-   - carg, cargf, cargl
-   - casin, casinf, casinl, casinh, casinhf, casinhl
-   - catan, catanf, catanl, catanh, catanhf, catanhl
-   - ccos, ccosf, ccosl, ccosh, ccoshf, ccoshl
-   - cexp, cexpf, cexpl
-   - cimag, cimagf, cimagl
-   - clog, clogf, clogl
-   - conj, conjf, conjl
-   - cpow, cpowf, cpowl
-   - cproj, cprojf, cprojl
-   - creal, crealf, creall
-   - csin, csinf, csinl, csinh, csinhf, csinhl
-   - csqrt, csqrtf, csqrtl
-   - ctan, ctanf, ctanl, ctanh, ctanhf, ctanhl
-*)
-
-(* [wint_t] isn't specified in [theMachine] so the following built-ins that
-   use this type can't be added :
-   - iswalnum
-   - iswalpha
-   - iswblank
-   - iswcntrl
-   - iswdigit
-   - iswgraph
-   - iswlower
-   - iswprint
-   - iswpunct
-   - iswspace
-   - iswupper
-   - iswxdigit
-   - towlower
-   - towupper
-*)
-
 let add_builtin_if_active b =
   if is_machdep_active b.compiler then begin
     Kernel.feedback ~dkey:Kernel.dkey_builtins