From eaa0741d9cb54cd0c309c48e205e15fec04b469f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 12 Jan 2022 11:37:11 +0100
Subject: [PATCH] [Kernel] move Cil_builtins declarations to JSON file and
 export as table

---
 Makefile                                      |    2 +
 headers/header_spec.txt                       |    1 +
 share/compliance/compiler_builtins.json       | 1865 +++++++++++++++++
 .../ast_queries/cil_builtins.ml               |  891 +++-----
 .../ast_queries/cil_builtins.mli              |   17 +
 .../plugin_entry_points/kernel.ml             |    2 +
 .../plugin_entry_points/kernel.mli            |    2 +
 tests/compliance/check-json.i                 |    3 +-
 tests/compliance/oracle/json_check-json_5.txt |    4 +-
 tests/compliance/oracle/json_check-json_6.txt |    2 +
 .../oracle/check_builtin_bts1440.res.oracle   |    6 +-
 11 files changed, 2201 insertions(+), 594 deletions(-)
 create mode 100644 share/compliance/compiler_builtins.json
 create mode 100644 tests/compliance/oracle/json_check-json_6.txt

diff --git a/Makefile b/Makefile
index c54f39e399b..3a6699dac5f 100644
--- a/Makefile
+++ b/Makefile
@@ -291,6 +291,7 @@ DISTRIB_FILES:=\
       share/_frama-c                                                    \
       share/compliance/c11_functions.json                               \
       share/compliance/c11_headers.json                                 \
+      share/compliance/compiler_builtins.json                           \
       share/compliance/glibc_functions.json                             \
       share/compliance/nonstandard_identifiers.json                     \
       share/compliance/posix_identifiers.json                           \
@@ -2007,6 +2008,7 @@ install:: install-lib-$(OCAMLBEST)
 	$(MKDIR) $(FRAMAC_DATADIR)/compliance
 	$(CP) share/compliance/c11_functions.json \
 	  share/compliance/c11_headers.json \
+	  share/compliance/compiler_builtins.json \
 	  share/compliance/glibc_functions.json \
 	  share/compliance/nonstandard_identifiers.json \
 	  share/compliance/posix_identifiers.json \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3c013f74b22..c7249748760 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -148,6 +148,7 @@ share/analysis-scripts/summary.py: CEA_LGPL
 share/analysis-scripts/template.mk: .ignore
 share/compliance/c11_functions.json: .ignore
 share/compliance/c11_headers.json: .ignore
+share/compliance/compiler_builtins.json: .ignore
 share/compliance/glibc_functions.json: .ignore
 share/compliance/nonstandard_identifiers.json: .ignore
 share/compliance/posix_identifiers.json: .ignore
diff --git a/share/compliance/compiler_builtins.json b/share/compliance/compiler_builtins.json
new file mode 100644
index 00000000000..cb51df655d7
--- /dev/null
+++ b/share/compliance/compiler_builtins.json
@@ -0,0 +1,1865 @@
+{
+    "description":"Compiler builtins supported by Frama-C",
+    "source":"Mostly https://gcc.gnu.org/onlinedocs/gcc/C-Extensions.html, from pages with 'Builtins' in their title",
+    "notes": {
+        "compiler":"When present, indicates this builtin is only available in Frama-C machdeps with this compiler. Allowed values: gcc, 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.",
+        "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":"Whether this builtin behaves as a variadic function."
+    },
+    "data":{
+        "__builtin__Exit": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin___fprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void *","int","char const *"],
+            "variadic":true
+        },
+        "__builtin___memcpy_chk": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","void const *","size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin___memmove_chk": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","void const *","size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin___mempcpy_chk": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","void const *","size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin___memset_chk": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","int","size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin___printf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int","char const *"],
+            "variadic":true
+        },
+        "__builtin___snprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","size_t","int","size_t","char const *"],
+            "variadic":true
+        },
+        "__builtin___sprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","int","size_t","char const *"],
+            "variadic":true
+        },
+        "__builtin___stpcpy_chk": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t"],
+            "variadic":false
+        },
+        "__builtin___strcat_chk": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t"],
+            "variadic":false
+        },
+        "__builtin___strcpy_chk": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t"],
+            "variadic":false
+        },
+        "__builtin___strncat_chk": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin___strncpy_chk": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin___vfprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void *","int","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin___vprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin___vsnprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","size_t","int","size_t","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin___vsprintf_chk": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","int","size_t","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_abs": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_acos": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_acosf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_acosh": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_acoshf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_acoshl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_acosl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_alloca": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["size_t"],
+            "variadic":false
+        },
+        "__builtin__annotation": {
+            "compiler":"msvc",
+            "rettype":"void",
+            "args": [],
+            "variadic":true
+        },
+        "__builtin_asin": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_asinf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_asinh": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_asinhf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_asinhl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_asinl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_atan": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_atan2": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_atan2f": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_atan2l": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_atanf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_atanh": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_atanhf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_atanhl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_atanl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_bswap16": {
+            "compiler":"gcc",
+            "rettype":"uint16_t",
+            "args": ["uint16_t"],
+            "variadic":false
+        },
+        "__builtin_bswap32": {
+            "compiler":"gcc",
+            "rettype":"uint32_t",
+            "args": ["uint32_t"],
+            "variadic":false
+        },
+        "__builtin_bswap64": {
+            "compiler":"gcc",
+            "rettype":"uint64_t",
+            "args": ["uint64_t"],
+            "variadic":false
+        },
+        "__builtin_calloc": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin_cbrt": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_cbrtf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_cbrtl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_ceil": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_ceilf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_ceill": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_constant_p": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_copysign": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_copysignf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_copysignl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_cos": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_cosf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_cosh": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_coshf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_coshl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_cosl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_erf": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_erfc": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_erfcf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_erfcl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_erff": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_erfl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_exit": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_exp": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_exp2": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_exp2f": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_exp2l": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_expect": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["long","long"],
+            "variadic":false
+        },
+        "__builtin_expf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_expl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_expm1": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_expm1f": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_expm1l": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_fabs": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_fabsf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_fabsl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_fdim": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_fdimf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_fdiml": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_ffs": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_ffsl": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["long"],
+            "variadic":false
+        },
+        "__builtin_ffsll": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["long long"],
+            "variadic":false
+        },
+        "__builtin_floor": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_floorf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_floorl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_fma": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double","double"],
+            "variadic":false
+        },
+        "__builtin_fmaf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float","float"],
+            "variadic":false
+        },
+        "__builtin_fmal": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double","long double"],
+            "variadic":false
+        },
+        "__builtin_fmax": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_fmaxf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_fmaxl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_fmin": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_fminf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_fminl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_fmod": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_fmodf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_fmodl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_fprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void *","char const *"],
+            "variadic":true
+        },
+        "__builtin_fputs": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","void *"],
+            "variadic":false
+        },
+        "__builtin_frame_address": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["unsigned int"],
+            "variadic":false
+        },
+        "__builtin_free": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": ["void *"],
+            "variadic":false
+        },
+        "__builtin_frexp": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","int *"],
+            "variadic":false
+        },
+        "__builtin_frexpf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","int *"],
+            "variadic":false
+        },
+        "__builtin_frexpl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","int *"],
+            "variadic":false
+        },
+        "__builtin_fscanf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void *","char const *"],
+            "variadic":true
+        },
+        "__builtin_huge_val": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_huge_valf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_huge_vall": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_hypot": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_hypotf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_hypotl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_ia32_lfence": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_ia32_mfence": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_ia32_sfence": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_ilogb": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_ilogbf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_ilogbl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_inf": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_inff": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_infl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_isalnum": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isalpha": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isblank": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_iscntrl": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isdigit": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isgraph": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_islower": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isprint": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_ispunct": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isspace": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isupper": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_isxdigit": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_labs": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["long"],
+            "variadic":false
+        },
+        "__builtin_ldexp": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","int"],
+            "variadic":false
+        },
+        "__builtin_ldexpf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","int"],
+            "variadic":false
+        },
+        "__builtin_ldexpl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","int"],
+            "variadic":false
+        },
+        "__builtin_lgamma": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_lgammaf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_lgammal": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_llabs": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["long long"],
+            "variadic":false
+        },
+        "__builtin_llrint": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_llrintf": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_llrintl": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_llround": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_llroundf": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_llroundl": {
+            "compiler":"gcc",
+            "rettype":"long long",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_log": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_log10": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_log10f": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_log10l": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_log1p": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_log1pf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_log1pl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_log2": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_log2f": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_log2l": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_logb": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_logbf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_logbl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_logf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_logl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_lrint": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_lrintf": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_lrintl": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_lround": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_lroundf": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_lroundl": {
+            "compiler":"gcc",
+            "rettype":"long",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_malloc": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["size_t"],
+            "variadic":false
+        },
+        "__builtin_memchr": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void const *","int","size_t"],
+            "variadic":false
+        },
+        "__builtin_memcmp": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void const *","void const *","size_t"],
+            "variadic":false
+        },
+        "__builtin_memcpy": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","void const *","size_t"],
+            "variadic":false
+        },
+        "__builtin_mempcpy": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","void const *","size_t"],
+            "variadic":false
+        },
+        "__builtin_memset": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","int","size_t"],
+            "variadic":false
+        },
+        "__builtin_modf": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double *"],
+            "variadic":false
+        },
+        "__builtin_modff": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float *"],
+            "variadic":false
+        },
+        "__builtin_modfl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double *"],
+            "variadic":false
+        },
+        "__builtin_nan": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_nanf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_nanl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_nans": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_nansf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_nansl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_nearbyint": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_nearbyintf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_nearbyintl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_nextafter": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_nextafterf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_nextafterl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_nexttoward": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","long double"],
+            "variadic":false
+        },
+        "__builtin_nexttowardf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","long double"],
+            "variadic":false
+        },
+        "__builtin_nexttowardl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_object_size": {
+            "compiler":"gcc",
+            "rettype":"size_t",
+            "args": ["void *","int"],
+            "variadic":false
+        },
+        "__builtin_offsetof": {
+            "rettype":"size_t",
+            "args": ["size_t"],
+            "variadic":false
+        },
+        "__builtin_parity": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["unsigned int"],
+            "variadic":false
+        },
+        "__builtin_parityl": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["unsigned long"],
+            "variadic":false
+        },
+        "__builtin_parityll": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["unsigned long long"],
+            "variadic":false
+        },
+        "__builtin_pow": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_powf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_powi": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","int"],
+            "variadic":false
+        },
+        "__builtin_powif": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","int"],
+            "variadic":false
+        },
+        "__builtin_powil": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","int"],
+            "variadic":false
+        },
+        "__builtin_powl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_prefetch": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": ["void const *"],
+            "variadic":true
+        },
+        "__builtin_printf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *"],
+            "variadic":true
+        },
+        "__builtin_putchar": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_puts": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_realloc": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["void *","size_t"],
+            "variadic":false
+        },
+        "__builtin_remainder": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double"],
+            "variadic":false
+        },
+        "__builtin_remainderf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float"],
+            "variadic":false
+        },
+        "__builtin_remainderl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double"],
+            "variadic":false
+        },
+        "__builtin_remquo": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","double","int *"],
+            "variadic":false
+        },
+        "__builtin_remquof": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","float","int *"],
+            "variadic":false
+        },
+        "__builtin_remquol": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long double","int *"],
+            "variadic":false
+        },
+        "__builtin_return": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": ["void const *"],
+            "variadic":false
+        },
+        "__builtin_return_address": {
+            "compiler":"gcc",
+            "rettype":"void *",
+            "args": ["unsigned int"],
+            "variadic":false
+        },
+        "__builtin_rint": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_rintf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_rintl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_round": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_roundf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_roundl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_scalbln": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","long"],
+            "variadic":false
+        },
+        "__builtin_scalblnf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","long"],
+            "variadic":false
+        },
+        "__builtin_scalblnl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","long"],
+            "variadic":false
+        },
+        "__builtin_scalbn": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double","int"],
+            "variadic":false
+        },
+        "__builtin_scalbnf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float","int"],
+            "variadic":false
+        },
+        "__builtin_scalbnl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double","int"],
+            "variadic":false
+        },
+        "__builtin_scanf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *"],
+            "variadic":true
+        },
+        "__builtin_sin": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_sinf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_sinh": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_sinhf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_sinhl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_sinl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_snprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","size_t","char const *"],
+            "variadic":true
+        },
+        "__builtin_sprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","char const *"],
+            "variadic":true
+        },
+        "__builtin_sqrt": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_sqrtf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_sqrtl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_sscanf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","char const *"],
+            "variadic":true
+        },
+        "__builtin_stdarg_start": {
+            "compiler":"!msvc",
+            "rettype":"void",
+            "args": ["__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_stpcpy": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strcat": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strchr": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","int"],
+            "variadic":false
+        },
+        "__builtin_strcmp": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strcpy": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strcspn": {
+            "compiler":"gcc",
+            "rettype":"size_t",
+            "args": ["char const *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strlen": {
+            "compiler":"gcc",
+            "rettype":"size_t",
+            "args": ["char const *"],
+            "variadic":false
+        },
+        "__builtin_strncat": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t"],
+            "variadic":false
+        },
+        "__builtin_strncmp": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","char const *","size_t"],
+            "variadic":false
+        },
+        "__builtin_strncpy": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char *","char const *","size_t"],
+            "variadic":false
+        },
+        "__builtin_strpbrk": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char const *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strrchr": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char const *","int"],
+            "variadic":false
+        },
+        "__builtin_strspn": {
+            "compiler":"gcc",
+            "rettype":"size_t",
+            "args": ["char const *","char const *"],
+            "variadic":false
+        },
+        "__builtin_strstr": {
+            "compiler":"gcc",
+            "rettype":"char *",
+            "args": ["char const *","char const *"],
+            "variadic":false
+        },
+        "__builtin_tan": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_tanf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_tanh": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_tanhf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_tanhl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_tanl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_tgamma": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_tgammaf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_tgammal": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_tolower": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_toupper": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["int"],
+            "variadic":false
+        },
+        "__builtin_trunc": {
+            "compiler":"gcc",
+            "rettype":"double",
+            "args": ["double"],
+            "variadic":false
+        },
+        "__builtin_truncf": {
+            "compiler":"gcc",
+            "rettype":"float",
+            "args": ["float"],
+            "variadic":false
+        },
+        "__builtin_truncl": {
+            "compiler":"gcc",
+            "rettype":"long double",
+            "args": ["long double"],
+            "variadic":false
+        },
+        "__builtin_types_compatible_p": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["size_t","size_t"],
+            "variadic":false
+        },
+        "__builtin_unreachable": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_va_arg": {
+            "compiler":"!msvc",
+            "rettype":"void",
+            "args": ["__builtin_va_list","size_t","void *"],
+            "variadic":false
+        },
+        "__builtin_va_copy": {
+            "compiler":"!msvc",
+            "rettype":"void",
+            "args": ["__builtin_va_list","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_va_end": {
+            "compiler":"!msvc",
+            "rettype":"void",
+            "args": ["__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_next_arg": {
+            "compiler":"!msvc",
+            "rettype":"__builtin_va_list",
+            "args": [],
+            "variadic":false
+        },
+        "__builtin_va_start": {
+            "compiler":"!msvc",
+            "rettype":"void",
+            "args": ["__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_varargs_start": {
+            "compiler":"!msvc",
+            "rettype":"void",
+            "args": ["__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vfprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void *","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vfscanf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["void *","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vscanf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vsnprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","size_t","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vsprintf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char *","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+        "__builtin_vsscanf": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["char const *","char const *","__builtin_va_list"],
+            "variadic":false
+        },
+
+        "__sync_add_and_fetch": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_and_and_fetch": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_bool_compare_and_swap": {
+            "compiler":"gcc",
+            "rettype":"int",
+            "args": ["type volatile *", "type", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_fetch_and_add": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_fetch_and_and": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_fetch_and_nand": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_fetch_and_or": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_fetch_and_sub": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_fetch_and_xor": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_lock_release": {
+            "compiler":"gcc",
+            "rettype":"void",
+            "args": ["type volatile *"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_lock_test_and_set": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_nand_and_fetch": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_or_and_fetch": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_sub_and_fetch": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_val_compare_and_swap": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *","type","type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        },
+        "__sync_xor_and_fetch": {
+            "compiler":"gcc",
+            "rettype":"type",
+            "args": ["type volatile *", "type"],
+            "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+            "variadic":true
+        }
+    }
+}
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index b990e16a029..a3c11a5f99e 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -100,484 +100,140 @@ let add_builtin ?(prefix="__builtin_") s t l b =
 
 let () = Cil.registerAttribute "FC_BUILTIN" (AttrName true)
 
-let intType = Cil.intType
-let voidPtrType = Cil.voidPtrType
-let charConstPtrType = Cil.charConstPtrType
-let voidConstPtrType = Cil.voidConstPtrType
-let charPtrType = Cil.charPtrType
-let voidType = Cil.voidType
-let floatType = Cil.floatType
-let doubleType = Cil.doubleType
-let longDoubleType = Cil.longDoubleType
-let longType = Cil.longType
-let longLongType = Cil.longLongType
-let uintType = Cil.uintType
-let ulongType = Cil.ulongType
-let ulongLongType = Cil.ulongLongType
-let intPtrType = Cil.intPtrType
-
-(* Initialize the builtin functions after the machine has been initialized. *)
-let initGccBuiltins () : unit =
-  (* 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 sizeType = Cil.theMachine.upointType in
-  let add = add_builtin in
-
-  add "__fprintf_chk"
-    intType
-    (* first argument is really FILE*, not void*, but we don't want to build in
-       the definition for FILE *)
-    [ voidPtrType; intType; charConstPtrType ]
-    true;
-  add "__memcpy_chk"
-    voidPtrType
-    [ voidPtrType; voidConstPtrType; sizeType; sizeType ]
-    false;
-  add "__memmove_chk"
-    voidPtrType [ voidPtrType; voidConstPtrType; sizeType; sizeType ] false;
-  add "__mempcpy_chk"
-    voidPtrType [ voidPtrType; voidConstPtrType; sizeType; sizeType ] false;
-  add "__memset_chk"
-    voidPtrType [ voidPtrType; intType; sizeType; sizeType ] false;
-  add "__printf_chk" intType [ intType; charConstPtrType ] true;
-  add "__snprintf_chk"
-    intType [ charPtrType; sizeType; intType; sizeType; charConstPtrType ]
-    true;
-  add "__sprintf_chk"
-    intType [ charPtrType; intType; sizeType; charConstPtrType ] true;
-  add "__stpcpy_chk"
-    charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
-  add "__strcat_chk"
-    charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
-  add "__strcpy_chk"
-    charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
-  add "__strncat_chk"
-    charPtrType [ charPtrType; charConstPtrType; sizeType; sizeType ] false;
-  add "__strncpy_chk"
-    charPtrType [ charPtrType; charConstPtrType; sizeType; sizeType ] false;
-  add "__vfprintf_chk"
-    intType
-    (* first argument is really FILE*, not void*, but we don't want to build in
-       the definition for FILE *)
-    [ voidPtrType; intType; charConstPtrType; TBuiltin_va_list [] ]
-    false;
-  add "__vprintf_chk"
-    intType [ intType; charConstPtrType; TBuiltin_va_list [] ] false;
-  add "__vsnprintf_chk"
-    intType
-    [ charPtrType; sizeType; intType; sizeType; charConstPtrType;
-      TBuiltin_va_list [] ]
-    false;
-  add "__vsprintf_chk"
-    intType
-    [ charPtrType; intType; sizeType; charConstPtrType; TBuiltin_va_list [] ]
-    false;
-
-  add "_Exit" voidType [ intType ] false;
-  add "exit" voidType [ intType ] false;
-
-  add "alloca" voidPtrType [ sizeType ] false;
-
-  add "malloc" voidPtrType [ sizeType ] false;
-  add "calloc" voidPtrType [ sizeType; sizeType ] false;
-  add "realloc" voidPtrType [ voidPtrType; sizeType ] false;
-  add "free" voidType [ voidPtrType ] false;
-
-  add "abs" intType [ intType ] false;
-  add "labs" longType [ longType ] false;
-  add "llabs" longLongType [ longLongType] false;
-  (* Can't add imaxabs because it takes intmax_t as parameter *)
-
-  add "acos" doubleType [ doubleType ] false;
-  add "acosf" floatType [ floatType ] false;
-  add "acosl" longDoubleType [ longDoubleType ] false;
-  add "acosh" doubleType [ doubleType ] false;
-  add "acoshf" floatType [ floatType ] false;
-  add "acoshl" longDoubleType [ longDoubleType ] false;
-
-  add "asin" doubleType [ doubleType ] false;
-  add "asinf" floatType [ floatType ] false;
-  add "asinl" longDoubleType [ longDoubleType ] false;
-  add "asinh" doubleType [ doubleType ] false;
-  add "asinhf" floatType [ floatType ] false;
-  add "asinhl" longDoubleType [ longDoubleType ] false;
-
-  add "atan" doubleType [ doubleType ] false;
-  add "atanf" floatType [ floatType ] false;
-  add "atanl" longDoubleType [ longDoubleType ] false;
-  add "atanh" doubleType [ doubleType ] false;
-  add "atanhf" floatType [ floatType ] false;
-  add "atanhl" longDoubleType [ longDoubleType ] false;
-
-  add "atan2" doubleType [ doubleType; doubleType ] false;
-  add "atan2f" floatType [ floatType; floatType ] false;
-  add "atan2l" longDoubleType [ longDoubleType;
-                                longDoubleType ] false;
-
-  let uint16t = Cil.uint16_t () in
-  add "bswap16" uint16t [uint16t] false;
-
-  let uint32t = Cil.uint32_t () in
-  add "bswap32" uint32t [uint32t] false;
-
-  let uint64t = Cil.uint64_t () in
-  add "bswap64" uint64t [uint64t] false;
-
-  add "cbrt" doubleType [ doubleType ] false;
-  add "cbrtf" floatType [ floatType ] false;
-  add "cbrtl" longDoubleType [ longDoubleType ] false;
-
-  add "ceil" doubleType [ doubleType ] false;
-  add "ceilf" floatType [ floatType ] false;
-  add "ceill" longDoubleType [ longDoubleType ] false;
-
-  add "cos" doubleType [ doubleType ] false;
-  add "cosf" floatType [ floatType ] false;
-  add "cosl" longDoubleType [ longDoubleType ] false;
-
-  add "cosh" doubleType [ doubleType ] false;
-  add "coshf" floatType [ floatType ] false;
-  add "coshl" longDoubleType [ longDoubleType ] false;
-
-  add "constant_p" intType [ intType ] false;
-
-  add "copysign" doubleType [ doubleType; doubleType ] false;
-  add "copysignf" floatType [ floatType; floatType ] false;
-  add "copysignl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "erfc" doubleType [ doubleType ] false;
-  add "erfcf" floatType [ floatType ] false;
-  add "erfcl" longDoubleType [ longDoubleType ] false;
-
-  add "erf" doubleType [ doubleType ] false;
-  add "erff" floatType [ floatType ] false;
-  add "erfl" longDoubleType [ longDoubleType ] false;
-
-  add "exp" doubleType [ doubleType ] false;
-  add "expf" floatType [ floatType ] false;
-  add "expl" longDoubleType [ longDoubleType ] false;
-
-  add "exp2" doubleType [ doubleType ] false;
-  add "exp2f" floatType [ floatType ] false;
-  add "exp2l" longDoubleType [ longDoubleType ] false;
-
-  add "expm1" doubleType [ doubleType ] false;
-  add "expm1f" floatType [ floatType ] false;
-  add "expm1l" longDoubleType [ longDoubleType ] false;
-
-  add "expect" longType [ longType; longType ] false;
-
-  add "fabs" doubleType [ doubleType ] false;
-  add "fabsf" floatType [ floatType ] false;
-  add "fabsl" longDoubleType [ longDoubleType ] false;
-
-  add "fdim" doubleType [ doubleType; doubleType ] false;
-  add "fdimf" floatType [ floatType; floatType ] false;
-  add "fdiml" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "ffs" intType [ uintType ] false;
-  add "ffsl" intType [ ulongType ] false;
-  add "ffsll" intType [ ulongLongType ] false;
-  add "frame_address" voidPtrType [ uintType ] false;
-
-  add "floor" doubleType [ doubleType ] false;
-  add "floorf" floatType [ floatType ] false;
-  add "floorl" longDoubleType [ longDoubleType ] false;
-
-  add "fma" doubleType [ doubleType; doubleType; doubleType ] false;
-  add "fmaf" floatType [ floatType; floatType; floatType ] false;
-  add "fmal"
-    longDoubleType [ longDoubleType; longDoubleType; longDoubleType ] false;
-
-  add "fmax" doubleType [ doubleType; doubleType ] false;
-  add "fmaxf" floatType [ floatType; floatType ] false;
-  add "fmaxl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "fmin" doubleType [ doubleType; doubleType ] false;
-  add "fminf" floatType [ floatType; floatType ] false;
-  add "fminl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "huge_val" doubleType [] false;
-  add "huge_valf" floatType [] false;
-  add "huge_vall" longDoubleType [] false;
-
-  add "hypot" doubleType [ doubleType; doubleType ] false;
-  add "hypotf" floatType [ floatType; floatType ] false;
-  add "hypotl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "ia32_lfence" voidType [] false;
-  add "ia32_mfence" voidType [] false;
-  add "ia32_sfence" voidType [] false;
-
-  add "ilogb" doubleType [ doubleType ] false;
-  add "ilogbf" floatType [ floatType ] false;
-  add "ilogbl" longDoubleType [ longDoubleType ] false;
-
-  add "inf" doubleType [] false;
-  add "inff" floatType [] false;
-  add "infl" longDoubleType [] false;
-
-  add "isblank" intType [ intType ] false;
-  add "isalnum" intType [ intType ] false;
-  add "isalpha" intType [ intType ] false;
-  add "iscntrl" intType [ intType ] false;
-  add "isdigit" intType [ intType ] false;
-  add "isgraph" intType [ intType ] false;
-  add "islower" intType [ intType ] false;
-  add "isprint" intType [ intType ] false;
-  add "ispunct" intType [ intType ] false;
-  add "isspace" intType [ intType ] false;
-  add "isupper" intType [ intType ] false;
-  add "isxdigit" intType [ intType ] false;
-
-  add "fmod" doubleType [ doubleType ] false;
-  add "fmodf" floatType [ floatType ] false;
-  add "fmodl" longDoubleType [ longDoubleType ] false;
-
-  add "frexp" doubleType [ doubleType; intPtrType ] false;
-  add "frexpf" floatType [ floatType; intPtrType  ] false;
-  add "frexpl" longDoubleType [ longDoubleType; intPtrType  ] false;
-
-  add "ldexp" doubleType [ doubleType; intType ] false;
-  add "ldexpf" floatType [ floatType; intType  ] false;
-  add "ldexpl" longDoubleType [ longDoubleType; intType  ] false;
-
-  add "lgamma" doubleType [ doubleType ] false;
-  add "lgammaf" floatType [ floatType ] false;
-  add "lgammal" longDoubleType [ longDoubleType ] false;
-
-  add "llrint" longLongType [ doubleType ] false;
-  add "llrintf" longLongType [ floatType ] false;
-  add "llrintl" longLongType [ longDoubleType ] false;
-
-  add "llround" longLongType [ doubleType ] false;
-  add "llroundf" longLongType [ floatType ] false;
-  add "llroundl" longLongType [ longDoubleType ] false;
-
-  add "log" doubleType [ doubleType ] false;
-  add "logf" floatType [ floatType ] false;
-  add "logl" longDoubleType [ longDoubleType ] false;
-
-  add "log10" doubleType [ doubleType ] false;
-  add "log10f" floatType [ floatType ] false;
-  add "log10l" longDoubleType [ longDoubleType ] false;
-
-  add "log1p" doubleType [ doubleType ] false;
-  add "log1pf" floatType [ floatType ] false;
-  add "log1pl" longDoubleType [ longDoubleType ] false;
-
-  add "log2" doubleType [ doubleType ] false;
-  add "log2f" floatType [ floatType ] false;
-  add "log2l" longDoubleType [ longDoubleType ] false;
-
-  add "logb" doubleType [ doubleType ] false;
-  add "logbf" floatType [ floatType ] false;
-  add "logbl" longDoubleType [ longDoubleType ] false;
-
-  add "lrint" longType [ doubleType ] false;
-  add "lrintf" longType [ floatType ] false;
-  add "lrintl" longType [ longDoubleType ] false;
-
-  add "lround" longType [ doubleType ] false;
-  add "lroundf" longType [ floatType ] false;
-  add "lroundl" longType [ longDoubleType ] false;
-
-  add "memchr" voidPtrType [ voidConstPtrType; intType; sizeType ] false;
-  add "memcmp" intType [ voidConstPtrType; voidConstPtrType; sizeType ] false;
-  add "memcpy" voidPtrType [ voidPtrType; voidConstPtrType; sizeType ] false;
-  add "mempcpy" voidPtrType [ voidPtrType; voidConstPtrType; sizeType ] false;
-  add "memset" voidPtrType [ voidPtrType; intType; sizeType ] false;
-
-  add "modf" doubleType [ doubleType; TPtr(doubleType,[]) ] false;
-  add "modff" floatType [ floatType; TPtr(floatType,[]) ] false;
-  add "modfl"
-    longDoubleType [ longDoubleType; TPtr(longDoubleType, []) ] false;
-
-  add "nan" doubleType [ charConstPtrType ] false;
-  add "nanf" floatType [ charConstPtrType ] false;
-  add "nanl" longDoubleType [ charConstPtrType ] false;
-  add "nans" doubleType [ charConstPtrType ] false;
-  add "nansf" floatType [ charConstPtrType ] false;
-  add "nansl" longDoubleType [ charConstPtrType ] false;
-
-  add "nearbyint" doubleType [ doubleType ] false;
-  add "nearbyintf" floatType [ floatType ] false;
-  add "nearbyintl" longDoubleType [ longDoubleType ] false;
-
-  add "nextafter" doubleType [ doubleType; doubleType ] false;
-  add "nextafterf" floatType [ floatType; floatType ] false;
-  add "nextafterl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "nexttoward" doubleType [ doubleType; longDoubleType ] false;
-  add "nexttowardf" floatType [ floatType; longDoubleType ] false;
-  add "nexttowardl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "object_size" sizeType [ voidPtrType; intType ] false;
-
-  add "parity" intType [ uintType ] false;
-  add "parityl" intType [ ulongType ] false;
-  add "parityll" intType [ ulongLongType ] false;
-
-  add "pow" doubleType [ doubleType; doubleType ] false;
-  add "powf" floatType [ floatType; floatType ] false;
-  add "powl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "powi" doubleType [ doubleType; intType ] false;
-  add "powif" floatType [ floatType; intType ] false;
-  add "powil" longDoubleType [ longDoubleType; intType ] false;
-
-  add "prefetch" voidType [ voidConstPtrType ] true;
-
-  add "printf" intType [ charConstPtrType ] true;
-  add "vprintf" intType [ charConstPtrType; TBuiltin_va_list [] ] false;
-  (* For [fprintf] and [vfprintf] the first argument is really FILE*, not void*,
-     but we don't want to build in the definition for FILE. *)
-  add "fprintf" intType [ voidPtrType; charConstPtrType ] true;
-  add "vfprintf"
-    intType [ voidPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
-  add "sprintf" intType [ charPtrType; charConstPtrType ] true;
-  add "vsprintf"
-    intType [ charPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
-  add "snprintf" intType [ charPtrType; sizeType; charConstPtrType ] true;
-  add "vsnprintf"
-    intType
-    [ charPtrType; sizeType; charConstPtrType; TBuiltin_va_list [] ]
-    false;
-
-  add "putchar" intType [ intType ] false;
-
-  add "puts" intType [ charConstPtrType ] false;
-  (* The second argument of [fputs] is really FILE*, not void*, but we
-     don't want to build in the definition for FILE. *)
-  add "fputs" intType [ charConstPtrType; voidPtrType ] false;
-
-  add "remainder" doubleType [ doubleType; doubleType ] false;
-  add "remainderf" floatType [ floatType; floatType ] false;
-  add "remainderl" longDoubleType [ longDoubleType; longDoubleType ] false;
-
-  add "remquo" doubleType [ doubleType; doubleType; intPtrType ] false;
-  add "remquof" floatType [ floatType; floatType; intPtrType ] false;
-  add "remquol"
-    longDoubleType [ longDoubleType; longDoubleType; intPtrType ] false;
-
-  add "return" voidType [ voidConstPtrType ] false;
-  add "return_address" voidPtrType [ uintType ] false;
-
-  add "rint" doubleType [ doubleType ] false;
-  add "rintf" floatType [ floatType ] false;
-  add "rintl" longDoubleType [ longDoubleType ] false;
-
-  add "round" doubleType [ doubleType ] false;
-  add "roundf" floatType [ floatType ] false;
-  add "roundl" longDoubleType [ longDoubleType ] false;
-
-  add "scalbln" doubleType [ doubleType; longType ] false;
-  add "scalblnf" floatType [ floatType; longType ] false;
-  add "scalblnl" longDoubleType [ longDoubleType; longType ] false;
-
-  add "scalbn" doubleType [ doubleType; intType ] false;
-  add "scalbnf" floatType [ floatType; intType ] false;
-  add "scalbnl" longDoubleType [ longDoubleType; intType ] false;
-
-  add "scanf" intType [ charConstPtrType ] true;
-  add "vscanf" intType [ charConstPtrType; TBuiltin_va_list [] ] false;
-  (* For [fscanf] and [vfscanf] the first argument is really FILE*, not void*,
-     but we don't want to build in the definition for FILE. *)
-  add "fscanf" intType [ voidPtrType; charConstPtrType ] true;
-  add "vfscanf"
-    intType [ voidPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
-  add "sscanf" intType [ charConstPtrType; charConstPtrType ] true;
-  add "vsscanf"
-    intType [ charConstPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
-
-  add "sin" doubleType [ doubleType ] false;
-  add "sinf" floatType [ floatType ] false;
-  add "sinl" longDoubleType [ longDoubleType ] false;
-
-  add "sinh" doubleType [ doubleType ] false;
-  add "sinhf" floatType [ floatType ] false;
-  add "sinhl" longDoubleType [ longDoubleType ] false;
-
-  add "sqrt" doubleType [ doubleType ] false;
-  add "sqrtf" floatType [ floatType ] false;
-  add "sqrtl" longDoubleType [ longDoubleType ] false;
-
-  add "stpcpy" charPtrType [ charPtrType; charConstPtrType ] false;
-  add "strcat" charPtrType [ charPtrType; charConstPtrType ] false;
-  add "strchr" charPtrType [ charPtrType; intType ] false;
-  add "strcmp" intType [ charConstPtrType; charConstPtrType ] false;
-  add "strcpy" charPtrType [ charPtrType; charConstPtrType ] false;
-  add "strcspn" sizeType [ charConstPtrType; charConstPtrType ] false;
-  add "strlen" sizeType [ charConstPtrType ] false;
-  add "strncat" charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
-  add "strncmp" intType [ charConstPtrType; charConstPtrType; sizeType ] false;
-  add "strncpy" charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
-  add "strspn" sizeType [ charConstPtrType; charConstPtrType ] false;
-  add "strpbrk" charPtrType [ charConstPtrType; charConstPtrType ] false;
-  add "strrchr" charPtrType [ charConstPtrType; intType ] false;
-  add "strstr" charPtrType [ charConstPtrType; charConstPtrType ] false;
-  (* When we parse builtin_types_compatible_p, we change its interface *)
-  add "types_compatible_p"
-    intType
-    [ Cil.theMachine.typeOfSizeOf;(* Sizeof the type *)
-      Cil.theMachine.typeOfSizeOf (* Sizeof the type *) ]
-    false;
-  add "tan" doubleType [ doubleType ] false;
-  add "tanf" floatType [ floatType ] false;
-  add "tanl" longDoubleType [ longDoubleType ] false;
-
-  add "tanh" doubleType [ doubleType ] false;
-  add "tanhf" floatType [ floatType ] false;
-  add "tanhl" longDoubleType [ longDoubleType ] false;
-
-  add "tgamma" doubleType [ doubleType ] false;
-  add "tgammaf" floatType [ floatType ] false;
-  add "tgammal" longDoubleType [ longDoubleType ] false;
-
-  add "tolower" intType [ intType ] false;
-  add "toupper" intType [ intType ] false;
-
-  add "trunc" doubleType [ doubleType ] false;
-  add "truncf" floatType [ floatType ] false;
-  add "truncl" longDoubleType [ longDoubleType ] false;
-
-  add "unreachable" voidType [ ] false;
+let custom_builtins = Queue.create ()
+
+let add_custom_builtin f = Queue.add f custom_builtins
 
+let register_custom_builtin (name, rt, prms, isva) =
+  Builtin_functions.add name (rt,prms,isva)
+
+(* Table Builtin_templates is similar to Builtin_functions,
+   but with a few differences:
+   1. it lists all _known_ builtins, even those not registered (available)
+      under the current machdep.
+   2. It lists the 'generic' builtin names, not their 'typed' versions,
+      e.g. '__sync_add_and_fetch' instead of '__sync_add_and_fetch_int32_t'.
+   3. It can refer to "generic" type 'type', as in GCC's docs, since its types
+      are only strings, not actual CIL types.
+   This table mirrors the contents of the 'data' field of file
+   'compiler_builtins.json'.
+*)
+
+type compiler = GCC | MSVC | Not_MSVC
+
+type builtin_template = {
+  name: string;
+  compiler: compiler option;
+  rettype: string;
+  args: string list;
+  types: string list option;
+  variadic: bool;
+}
+
+let to_compiler s =
+  if s = "gcc" then GCC
+  else if s = "msvc" then MSVC
+  else if s = "!msvc" then Not_MSVC
+  else
+    Kernel.fatal "invalid compiler '%s' in compiler_builtins JSON" s
+
+let string_of_compiler = function
+  | GCC -> "GCC-based"
+  | MSVC -> "MSVC-based"
+  | Not_MSVC -> "not MSVC-based"
+
+module Builtin_template = struct
+  let dummy =
+    { name = "";
+      compiler = None;
+      rettype = "";
+      args = [];
+      types = None;
+      variadic = false;
+    }
+  include Datatype.Make_with_collections
+      (struct
+        type t = builtin_template
+        let name = "Builtin_template"
+        let reprs = [ dummy ]
+        let compare b1 b2 = String.compare b1.name b2.name
+        let hash b = Datatype.String.hash b.name
+        let equal b1 b2 = b1.name = b2.name
+        let copy = Datatype.identity
+        let internal_pretty_code = Datatype.undefined
+        let pretty fmt b =
+          Format.fprintf fmt "%s %s(%a%s)"
+            b.rettype b.name
+            (Pretty_utils.pp_list ~sep:", " Format.pp_print_string) b.args
+            (if b.variadic then ", ..." else "")
+        let rehash = Datatype.identity
+        let structural_descr = Structural_descr.t_abstract
+        let mem_project = Datatype.never_any_project
+        let varname b = "_cb_" ^ b.name
+      end)
+end
+module Builtin_templates =
+  State_builder.Hashtbl
+    (Datatype.String.Hashtbl)
+    (Builtin_template)
+    (struct
+      let name = "Builtin_templates"
+      let dependencies = []
+      let size = 200
+    end)
+
+(* An actual instance of a builtin_template, with actual types. *)
+type builtin = {
+  name: string;
+  compiler: compiler option;
+  rettype: typ option;
+  args: typ option list;
+  variadic: bool;
+}
+
+module Json =
+struct
+  open Yojson.Basic
+  open Util
+
+  let parse fp =
+    Kernel.feedback ~dkey:Kernel.dkey_builtins "Parsing builtins file: %a"
+      Datatype.Filepath.pretty fp;
+    let json = Json.from_file fp in
+    member "data" json
+
+  let init_builtin_templates () =
+    let fp =
+      Datatype.Filepath.concat ~existence:Filepath.Must_exist
+        Fc_config.datadir "compliance/compiler_builtins.json"
+    in
+    let json = parse fp in
+    List.iter (fun (name, entry) ->
+        let compiler =
+          entry |> member "compiler" |> to_string_option |>
+          Option.map to_compiler
+        in
+        let rettype = entry |> member "rettype" |> to_string in
+        let args = entry |> member "args" |> to_list |> List.map to_string in
+        let variadic = entry |> member "variadic" |> to_bool in
+        let types =
+          match entry |> member "types" with
+          | `Null -> None
+          | `List l -> Some (List.map to_string l)
+          | _ ->
+            Kernel.fatal "invalid 'types': expected list (in %a)"
+              Datatype.Filepath.pretty fp
+        in
+        let cb = { name; compiler; rettype; args; types; variadic} in
+        Builtin_templates.replace name cb
+      ) (json |> to_assoc)
+
+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. *)
+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
   let int32_t = try Some (Cil.int32_t ()) with Not_found -> None in
@@ -586,126 +242,185 @@ let initGccBuiltins () : unit =
   let uint16_t = try Some (Cil.uint16_t ()) with Not_found -> None in
   let uint32_t = try Some (Cil.uint32_t ()) with Not_found -> None in
   let uint64_t = try Some (Cil.uint64_t ()) with Not_found -> None in
-
-  (* Binary monomorphic versions of atomic builtins *)
-  let atomic_instances =
-    [int8_t, "_int8_t";
-     int16_t,"_int16_t";
-     int32_t,"_int32_t";
-     int64_t,"_int64_t";
-     uint8_t, "_uint8_t";
-     uint16_t,"_uint16_t";
-     uint32_t,"_uint32_t";
-     uint64_t,"_uint64_t"]
-  in
-  let add_sync (typ,name) f =
-    match typ with
-    | Some typ ->
-      add ~prefix:"__sync_" (f^name) typ [ TPtr(typeAddVolatile typ,[]); typ] true
-    | None -> ()
-  in
-  let add_sync f =
-    List.iter (fun typ -> add_sync typ f) atomic_instances
-  in
-  add_sync "fetch_and_add";
-  add_sync "fetch_and_sub";
-  add_sync "fetch_and_or";
-  add_sync "fetch_and_and";
-  add_sync "fetch_and_xor";
-  add_sync "fetch_and_nand";
-  add_sync "add_and_fetch";
-  add_sync "sub_and_fetch";
-  add_sync "or_and_fetch";
-  add_sync "and_and_fetch";
-  add_sync "xor_and_fetch";
-  add_sync "nand_and_fetch";
-  add_sync "lock_test_and_set";
-  List.iter (fun (typ,n) ->
-      match typ with
-      | Some typ ->
-        add ~prefix:"" ("__sync_bool_compare_and_swap"^n)
-          intType
-          [ TPtr(typeAddVolatile typ,[]); typ ; typ]
-          true
-      | None -> ())
-    atomic_instances;
-  List.iter (fun (typ,n) ->
-      match typ with
-      | Some typ ->
-        add ~prefix:"" ("__sync_val_compare_and_swap"^n)
-          typ
-          [ TPtr(typeAddVolatile typ,[]); typ ; typ]
-          true
-      | None -> ())
-    atomic_instances;
-  List.iter (fun (typ,n) ->
-      match typ with
-      | Some typ ->
-        add ~prefix:"" ("__sync_lock_release"^n)
-          voidType
-          [ TPtr(typeAddVolatile typ,[]) ]
-          true;
-      | None -> ())
-    atomic_instances;
-  (* __sync_synchronize has been declared non-variadic and a spec was added
-     to __fc_gcc_builtins.h; to avoid issues with pretty-printing, we removed
-     it from this list. *)
-;;
-
-(* Builtins related to va_list. Added to all non-msvc machdeps, because
-   Cabs2cil supposes they exist. *)
-let initVABuiltins () =
-  let hasbva = Cil.theMachine.theMachine.has__builtin_va_list in
-  let add = add_builtin in
-  add "next_arg"
-    (* When we parse builtin_next_arg we drop the second argument *)
-    (if hasbva then TBuiltin_va_list [] else voidPtrType) [] false;
-  if hasbva then begin
-    add "va_end" voidType [ TBuiltin_va_list [] ] false;
-    add "varargs_start" voidType [ TBuiltin_va_list [] ] false;
-    (* When we parse builtin_{va,stdarg}_start, we drop the second argument *)
-    add "va_start" voidType [ TBuiltin_va_list [] ] false;
-    add "stdarg_start" voidType [ TBuiltin_va_list [] ] false;
-    (* When we parse builtin_va_arg we change its interface *)
-    add "va_arg"
-      voidType
-      [ TBuiltin_va_list [];
-        Cil.theMachine.typeOfSizeOf;(* Sizeof the type *)
-        voidPtrType (* Ptr to res *) ]
-      false;
-    add "va_copy" voidType [ TBuiltin_va_list []; TBuiltin_va_list [] ] false;
+  let ptr_of = Option.map (fun t -> TPtr(t,[])) in
+  let volatile_ptr_of = Option.map (fun t -> TPtr(typeAddVolatile t,[])) in
+  let types =
+    [
+      ("__builtin_va_list",
+       Some (if Cil.theMachine.theMachine.has__builtin_va_list
+             then TBuiltin_va_list []
+             else Cil.voidPtrType));
+      ("char *", Some Cil.charPtrType);
+      ("char const *", Some Cil.charConstPtrType);
+      ("double", Some Cil.doubleType);
+      ("double *", Some (TPtr(Cil.doubleType,[])));
+      ("float", Some Cil.floatType);
+      ("float *", Some (TPtr(Cil.floatType,[])));
+      ("int", Some Cil.intType);
+      ("int *", Some Cil.intPtrType);
+      ("int volatile *", Some (TPtr(typeAddVolatile Cil.intType,[])));
+      ("long", Some Cil.longType);
+      ("long double", Some Cil.longDoubleType);
+      ("long double *", Some (TPtr(Cil.longDoubleType,[])));
+      ("long long", Some Cil.longLongType);
+      ("long long volatile *", Some (TPtr(typeAddVolatile Cil.longLongType,[])));
+      ("short", Some Cil.shortType);
+      ("short volatile *", Some (TPtr(typeAddVolatile Cil.shortType,[])));
+      ("signed char", Some Cil.scharType);
+      ("signed char volatile *", Some (TPtr(typeAddVolatile Cil.scharType,[])));
+      ("unsigned char", Some Cil.ucharType);
+      ("unsigned char volatile *", Some (TPtr(typeAddVolatile Cil.ucharType,[])));
+      ("unsigned int", Some Cil.uintType);
+      ("unsigned int volatile *", Some (TPtr(typeAddVolatile Cil.uintType,[])));
+      ("unsigned long", Some Cil.ulongType);
+      ("unsigned long long", Some Cil.ulongLongType);
+      ("unsigned long long volatile *", Some (TPtr(typeAddVolatile Cil.ulongLongType,[])));
+      ("unsigned short", Some Cil.ushortType);
+      ("unsigned short volatile *", Some (TPtr(typeAddVolatile Cil.ushortType,[])));
+      ("void", Some Cil.voidType);
+      ("void *", Some Cil.voidPtrType);
+      ("void const *", Some Cil.voidConstPtrType);
+      ("size_t", Some Cil.theMachine.typeOfSizeOf);
+      ("int8_t", int8_t);
+      ("int16_t", int16_t);
+      ("int32_t", int32_t);
+      ("int64_t", int64_t);
+      ("uint8_t", uint8_t);
+      ("uint16_t", uint16_t);
+      ("uint32_t", uint32_t);
+      ("uint64_t", uint64_t);
+      ("int8_t *", ptr_of int8_t);
+      ("int16_t *", ptr_of int16_t);
+      ("int32_t *", ptr_of int32_t);
+      ("int64_t *", ptr_of int64_t);
+      ("uint8_t *", ptr_of uint8_t);
+      ("uint16_t *", ptr_of uint16_t);
+      ("uint32_t *", ptr_of uint32_t);
+      ("uint64_t *", ptr_of uint64_t);
+      ("int8_t volatile *", volatile_ptr_of int8_t);
+      ("int16_t volatile *", volatile_ptr_of int16_t);
+      ("int32_t volatile *", volatile_ptr_of int32_t);
+      ("int64_t volatile *", volatile_ptr_of int64_t);
+      ("uint8_t volatile *", volatile_ptr_of uint8_t);
+      ("uint16_t volatile *", volatile_ptr_of uint16_t);
+      ("uint32_t volatile *", volatile_ptr_of uint32_t);
+      ("uint64_t volatile *", volatile_ptr_of uint64_t);
+    ] in
+  Hashtbl.of_seq (List.to_seq types)
+
+let parse_type ?(template="") type_table s =
+  try
+    if Extlib.string_prefix "type" s then
+      (* replace 'type' (always at the beginning) with the template *)
+      let typ = template ^ (String.sub s 4 (String.length s - 4)) in
+      Hashtbl.find type_table typ
+    else
+      Hashtbl.find type_table s
+  with Not_found ->
+    Kernel.fatal "invalid type '%s' in compiler_builtins JSON" s
+
+let is_machdep_active compiler =
+  match compiler, Cil.gccMode (), Cil.msvcMode () with
+  | None, _, _ (* always active *)
+  | Some GCC, true, _
+  | Some MSVC, _, true
+  | 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
+      "adding builtin: %a %s(%a%s)"
+      Cil_datatype.Typ.pretty (Option.get b.rettype) b.name
+      (Pretty_utils.pp_list ~sep:", " Cil_datatype.Typ.pretty)
+      (List.map Option.get b.args)
+      (if b.variadic then ", ..." else "")
+    ;
+    add_builtin ~prefix:"" b.name (Option.get b.rettype)
+      ((List.map Option.get) b.args) b.variadic
   end
 
-let initMsvcBuiltins () : unit =
-  (** Take a number of wide string literals *)
-  Builtin_functions.add "__annotation" (voidType, [ ], true)
-
-let init_common_builtins () =
-  add_builtin
-    "offsetof"
-    Cil.theMachine.typeOfSizeOf
-    [ Cil.theMachine.typeOfSizeOf ]
-    false
-
-let custom_builtins = Queue.create ()
-
-let add_custom_builtin f = Queue.add f custom_builtins
+(* Instantiates builtins according to the types in the template.
+   In some machdeps, there may be missing types (e.g. int16_t);
+   such elements are not instantiated in the resulting list.
+   If the template has no 'types' member, at most a single
+   builtin will be instantiated. *)
+let instantiate_available_templates type_table name (entry : builtin_template) =
+  let compiler = entry.compiler in
+  let variadic = entry.variadic in
+  let make_builtin_as_list ?template name =
+    let to_type_opt = parse_type ?template type_table in
+    let rettype = to_type_opt entry.rettype in
+    let args = List.map to_type_opt entry.args in
+    if rettype = None || List.exists (fun arg -> arg = None) args
+    then (* unavailable type: skip builtin *) []
+    else
+      let name =
+        Option.fold ~none:name ~some:(fun t -> name ^ "_" ^ t) template
+      in
+      [{ name; compiler; rettype; args; variadic }]
+  in
+  match entry.types with
+  | Some types ->
+    List.fold_left (fun acc template ->
+        (make_builtin_as_list ~template name) @ acc
+      ) [] types
+  | None ->
+    make_builtin_as_list name
 
-let register_custom_builtin (name, rt, prms, isva) =
-  Builtin_functions.add name (rt,prms,isva)
+let init_builtins () =
+  Json.init_builtin_templates ();
+  let type_table = build_type_table () in
+  Builtin_templates.iter (fun name entry ->
+      (* In the JSON file, each entry is possibly a template for
+         several type-specialized functions *)
+      let builtins = instantiate_available_templates type_table name entry in
+      List.iter add_builtin_if_active builtins
+    )
 
 let init_builtins () =
   if not (Cil.selfMachine_is_computed ()) then
     Kernel.fatal ~current:true "You must call initCIL before init_builtins" ;
   if Builtin_functions.length () <> 0 then
     Kernel.fatal ~current:true "Cil builtins already initialized." ;
-  init_common_builtins ();
-  if Cil.msvcMode () then
-    initMsvcBuiltins ()
-  else begin
-    initVABuiltins ();
-    if Cil.gccMode () then initGccBuiltins ();
-  end;
+  init_builtins ();
   Queue.iter (fun f -> register_custom_builtin (f())) custom_builtins
 
 (** This is used as the location of the prototypes of builtin functions. *)
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
index 3c08e8507bc..5ec4bf598d2 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -95,6 +95,23 @@ module Builtin_functions :
   State_builder.Hashtbl with type key = string
                          and type data = typ * typ list * bool
 
+type compiler = GCC | MSVC | Not_MSVC
+
+val string_of_compiler : compiler -> string
+
+type builtin_template = {
+  name: string;
+  compiler: compiler option;
+  rettype: string;
+  args: string list;
+  types: string list option;
+  variadic: bool;
+}
+
+module Builtin_templates :
+  State_builder.Hashtbl with type key = string
+                         and type data = builtin_template
+
 (** Register a new builtin. The function will be called after setting
     the machdep and initializing machine-dependent builtins. Hence, types
     such {!Cil.uint16_t} might be used if needed.
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 69334701d76..68dc8ea3c71 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -46,6 +46,8 @@ let dkey_asm_contracts = register_category "asm:contracts"
 
 let dkey_ast = register_category "ast"
 
+let dkey_builtins = register_category "builtins"
+
 let dkey_check = register_category "check"
 
 let dkey_constfold = register_category "constfold"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index fda42e772bc..35ff0f29c84 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -41,6 +41,8 @@ val dkey_asm_contracts: category
 
 val dkey_ast: category
 
+val dkey_builtins: category
+
 val dkey_check: category
 
 val dkey_constfold: category
diff --git a/tests/compliance/check-json.i b/tests/compliance/check-json.i
index c9e5ac23e74..80c4d1a9d80 100644
--- a/tests/compliance/check-json.i
+++ b/tests/compliance/check-json.i
@@ -5,5 +5,6 @@
   EXECNOW: LOG json_@PTEST_NAME@_2.txt python3 -m json.tool < @SHARE@/glibc_functions.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_2.txt 2> @DEV_NULL@
   EXECNOW: LOG json_@PTEST_NAME@_3.txt python3 -m json.tool < @SHARE@/nonstandard_identifiers.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_3.txt 2> @DEV_NULL@
   EXECNOW: LOG json_@PTEST_NAME@_4.txt python3 -m json.tool < @SHARE@/posix_identifiers.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_4.txt 2> @DEV_NULL@
-  EXECNOW: LOG json_@PTEST_NAME@_5.txt python3 @PTEST_DIR@/sanity-checks.py @SHARE@ > @PTEST_RESULT@/json_@PTEST_NAME@_5.txt 2> @DEV_NULL@
+  EXECNOW: LOG json_@PTEST_NAME@_5.txt python3 -m json.tool < @SHARE@/compiler_builtins.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_5.txt 2> @DEV_NULL@
+  EXECNOW: LOG json_@PTEST_NAME@_6.txt python3 @PTEST_DIR@/sanity-checks.py @SHARE@ > @PTEST_RESULT@/json_@PTEST_NAME@_6.txt 2> @DEV_NULL@
 */
diff --git a/tests/compliance/oracle/json_check-json_5.txt b/tests/compliance/oracle/json_check-json_5.txt
index 295b7a131d2..431457d543b 100644
--- a/tests/compliance/oracle/json_check-json_5.txt
+++ b/tests/compliance/oracle/json_check-json_5.txt
@@ -1,2 +1,2 @@
-posix_identifiers.json checked.
-c11_functions.json checked.
+{
+    "description": "Compiler builtins supported by Frama-C",
diff --git a/tests/compliance/oracle/json_check-json_6.txt b/tests/compliance/oracle/json_check-json_6.txt
new file mode 100644
index 00000000000..295b7a131d2
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_6.txt
@@ -0,0 +1,2 @@
+posix_identifiers.json checked.
+c11_functions.json checked.
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 32d925b4bfe..d115b107f7d 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -183,11 +183,11 @@
   
   long double __builtin_fdiml(long double __x0, long double __x1);
   
-  int __builtin_ffs(unsigned int __x0);
+  int __builtin_ffs(int __x0);
   
-  int __builtin_ffsl(unsigned long __x0);
+  int __builtin_ffsl(long __x0);
   
-  int __builtin_ffsll(unsigned long long __x0);
+  int __builtin_ffsll(long long __x0);
   
   double __builtin_floor(double __x0);
   
-- 
GitLab