diff --git a/share/compliance/compiler_builtins.json b/share/compliance/compiler_builtins.json index 2aca1737576bfa2e6e9a85988f519e85d26ed6be..165d82ddd38486cf81fa435d8f0115223ae8cc6c 100644 --- a/share/compliance/compiler_builtins.json +++ b/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": { diff --git a/share/compliance/gcc_builtins.json b/share/compliance/gcc_builtins.json index 860027309d28c5c7e83d0b5b1a0483ae1b4ecc21..9e240b0ab214c0592e667880d6fa06ba64dcc252 100644 --- a/share/compliance/gcc_builtins.json +++ b/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": { diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml index 76fbb26e89423910b4331e8961f1d717c80f9899..4d0545f91f3f05c0e4251f395a25a5748f373bbe 100644 --- a/src/kernel_services/ast_queries/cil_builtins.ml +++ b/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