diff --git a/Makefile b/Makefile
index c54f39e399b32a633f7813b61110e81211f1ad1e..c4185f9379adc3ba190abf24083fada13956da0a 100644
--- a/Makefile
+++ b/Makefile
@@ -291,6 +291,8 @@ DISTRIB_FILES:=\
share/_frama-c \
share/compliance/c11_functions.json \
share/compliance/c11_headers.json \
+ share/compliance/compiler_builtins.json \
+ share/compliance/gcc_builtins.json \
share/compliance/glibc_functions.json \
share/compliance/nonstandard_identifiers.json \
share/compliance/posix_identifiers.json \
@@ -2007,6 +2009,8 @@ 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/gcc_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 3c013f74b22470bbbd8b35de055ce034a8b8f281..75a8014972c92d933188bcb17480f0c050a7ab7f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -148,6 +148,8 @@ 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/gcc_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 0000000000000000000000000000000000000000..165d82ddd38486cf81fa435d8f0115223ae8cc6c
--- /dev/null
+++ b/share/compliance/compiler_builtins.json
@@ -0,0 +1,57 @@
+{
+ "description":"Compiler builtins supported by Frama-C (for GCC builtins, see gcc_builtins.json)",
+ "notes": {
+ "compiler":"When present, indicates this builtin is only available in Frama-C machdeps with this compiler. Allowed values: msvc, !msvc (the latter meaning: 'available in machdeps with compilers other than MSVC').",
+ "rettype":"Return type of the builtin. Whitespace is important: types are matched as exact strings, with a single space between components.",
+ "args":"List of the types of the builtin arguments. Whitespace is important: types are matched as exact strings, with a single space between components.",
+ "variadic":"When present, this builtin behaves as a variadic function.",
+ "_comment": "Adding new types to fields 'rettype' or 'args' requires updating the list of recognized types in 'src/kernel_services/ast_queries/cil_builtins.ml'."
+ },
+ "data":{
+ "__builtin__annotation": {
+ "compiler":"msvc",
+ "rettype":"void",
+ "args": [],
+ "variadic":true
+ },
+ "__builtin_next_arg": {
+ "compiler":"!msvc",
+ "rettype":"__builtin_va_list",
+ "args": []
+ },
+ "__builtin_offsetof": {
+ "rettype":"size_t",
+ "args": ["size_t"]
+ },
+ "__builtin_stdarg_start": {
+ "compiler":"!msvc",
+ "rettype":"void",
+ "args": ["__builtin_va_list"]
+ },
+ "__builtin_va_arg": {
+ "compiler":"!msvc",
+ "rettype":"void",
+ "args": ["__builtin_va_list","size_t","void *"]
+ },
+ "__builtin_va_copy": {
+ "compiler":"!msvc",
+ "rettype":"void",
+ "args": ["__builtin_va_list","__builtin_va_list"]
+ },
+ "__builtin_va_end": {
+ "compiler":"!msvc",
+ "rettype":"void",
+ "args": ["__builtin_va_list"]
+ },
+ "__builtin_va_start": {
+ "compiler":"!msvc",
+ "rettype":"void",
+ "args": ["__builtin_va_list"]
+ },
+ "__builtin_varargs_start": {
+ "compiler":"!msvc",
+ "rettype":"void",
+ "args": ["__builtin_va_list"]
+ }
+ }
+}
diff --git a/share/compliance/gcc_builtins.json b/share/compliance/gcc_builtins.json
new file mode 100644
index 0000000000000000000000000000000000000000..9e240b0ab214c0592e667880d6fa06ba64dcc252
--- /dev/null
+++ b/share/compliance/gcc_builtins.json
@@ -0,0 +1,1336 @@
+{
+ "description":"GCC builtins supported by Frama-C",
+ "source":"Mostly https://gcc.gnu.org/onlinedocs/gcc/C-Extensions.html, from pages with 'Builtins' in their title",
+ "notes": {
+ "rettype":"Return type of the builtin. Whitespace is important: types are matched as exact strings, with a single space between components.",
+ "args":"List of the types of the builtin arguments. Whitespace is important: types are matched as exact strings, with a single space between components. The full list of 'known' type names is available in cil_builtins.ml.",
+ "types":"When present, a list indicating that this is a builtin template, to be instantiated for each type in the list. Instantiation is the replacement of each occurrence of 'type' in 'rettype' and 'args' with the elements of this list.",
+ "variadic":"When present, this builtin behaves as a variadic function.",
+ "_comment": [
+ "Complex types are unsupported, so the following builtins cannot be added:",
+ "cabs",
+ "cabsf",
+ "cabsh",
+ "cacos",
+ "cacosf",
+ "cacosl",
+ "cacosh",
+ "cacoshf",
+ "cacoshl",
+ "carg",
+ "cargf",
+ "cargl",
+ "casin",
+ "casinf",
+ "casinl",
+ "casinh",
+ "casinhf",
+ "casinhl",
+ "catan",
+ "catanf",
+ "catanl",
+ "catanh",
+ "catanhf",
+ "catanhl",
+ "ccos",
+ "ccosf",
+ "ccosl",
+ "ccosh",
+ "ccoshf",
+ "ccoshl",
+ "cexp",
+ "cexpf",
+ "cexpl",
+ "cimag",
+ "cimagf",
+ "cimagl",
+ "clog",
+ "clogf",
+ "clogl",
+ "conj",
+ "conjf",
+ "conjl",
+ "cpow",
+ "cpowf",
+ "cpowl",
+ "cproj",
+ "cprojf",
+ "cprojl",
+ "creal",
+ "crealf",
+ "creall",
+ "csin",
+ "csinf",
+ "csinl",
+ "csinh",
+ "csinhf",
+ "csinhl",
+ "csqrt",
+ "csqrtf",
+ "csqrtl",
+ "ctan",
+ "ctanf",
+ "ctanl",
+ "ctanh",
+ "ctanhf",
+ "ctanhl",
+ "Also, the type 'wint_t' is not specified in 'theMachine', so the following builtins that use it cannot be added:",
+ "iswalnum",
+ "iswalpha",
+ "iswblank",
+ "iswcntrl",
+ "iswdigit",
+ "iswgraph",
+ "iswlower",
+ "iswprint",
+ "iswpunct",
+ "iswspace",
+ "iswupper",
+ "iswxdigit",
+ "towlower",
+ "towupper"
+ ]
+ },
+ "data":{
+ "__builtin__Exit": {
+ "rettype":"void",
+ "args": ["int"]
+ },
+ "__builtin___fprintf_chk": {
+ "rettype":"int",
+ "args": ["void *","int","char const *"],
+ "variadic":true
+ },
+ "__builtin___memcpy_chk": {
+ "rettype":"void *",
+ "args": ["void *","void const *","size_t","size_t"]
+ },
+ "__builtin___memmove_chk": {
+ "rettype":"void *",
+ "args": ["void *","void const *","size_t","size_t"]
+ },
+ "__builtin___mempcpy_chk": {
+ "rettype":"void *",
+ "args": ["void *","void const *","size_t","size_t"]
+ },
+ "__builtin___memset_chk": {
+ "rettype":"void *",
+ "args": ["void *","int","size_t","size_t"]
+ },
+ "__builtin___printf_chk": {
+ "rettype":"int",
+ "args": ["int","char const *"],
+ "variadic":true
+ },
+ "__builtin___snprintf_chk": {
+ "rettype":"int",
+ "args": ["char *","size_t","int","size_t","char const *"],
+ "variadic":true
+ },
+ "__builtin___sprintf_chk": {
+ "rettype":"int",
+ "args": ["char *","int","size_t","char const *"],
+ "variadic":true
+ },
+ "__builtin___stpcpy_chk": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t"]
+ },
+ "__builtin___strcat_chk": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t"]
+ },
+ "__builtin___strcpy_chk": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t"]
+ },
+ "__builtin___strncat_chk": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t","size_t"]
+ },
+ "__builtin___strncpy_chk": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t","size_t"]
+ },
+ "__builtin___vfprintf_chk": {
+ "rettype":"int",
+ "args": ["void *","int","char const *","__builtin_va_list"]
+ },
+ "__builtin___vprintf_chk": {
+ "rettype":"int",
+ "args": ["int","char const *","__builtin_va_list"]
+ },
+ "__builtin___vsnprintf_chk": {
+ "rettype":"int",
+ "args": ["char *","size_t","int","size_t","char const *","__builtin_va_list"]
+ },
+ "__builtin___vsprintf_chk": {
+ "rettype":"int",
+ "args": ["char *","int","size_t","char const *","__builtin_va_list"]
+ },
+ "__builtin_abs": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_acos": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_acosf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_acosh": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_acoshf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_acoshl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_acosl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_alloca": {
+ "rettype":"void *",
+ "args": ["size_t"]
+ },
+ "__builtin_asin": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_asinf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_asinh": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_asinhf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_asinhl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_asinl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_atan": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_atan2": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_atan2f": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_atan2l": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_atanf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_atanh": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_atanhf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_atanhl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_atanl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_bswap16": {
+ "rettype":"uint16_t",
+ "args": ["uint16_t"]
+ },
+ "__builtin_bswap32": {
+ "rettype":"uint32_t",
+ "args": ["uint32_t"]
+ },
+ "__builtin_bswap64": {
+ "rettype":"uint64_t",
+ "args": ["uint64_t"]
+ },
+ "__builtin_calloc": {
+ "rettype":"void *",
+ "args": ["size_t","size_t"]
+ },
+ "__builtin_cbrt": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_cbrtf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_cbrtl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_ceil": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_ceilf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_ceill": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_constant_p": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_copysign": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_copysignf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_copysignl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_cos": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_cosf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_cosh": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_coshf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_coshl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_cosl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_erf": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_erfc": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_erfcf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_erfcl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_erff": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_erfl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_exit": {
+ "rettype":"void",
+ "args": ["int"]
+ },
+ "__builtin_exp": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_exp2": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_exp2f": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_exp2l": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_expect": {
+ "rettype":"long",
+ "args": ["long","long"]
+ },
+ "__builtin_expf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_expl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_expm1": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_expm1f": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_expm1l": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_fabs": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_fabsf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_fabsl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_fdim": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_fdimf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_fdiml": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_ffs": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_ffsl": {
+ "rettype":"int",
+ "args": ["long"]
+ },
+ "__builtin_ffsll": {
+ "rettype":"int",
+ "args": ["long long"]
+ },
+ "__builtin_floor": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_floorf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_floorl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_fma": {
+ "rettype":"double",
+ "args": ["double","double","double"]
+ },
+ "__builtin_fmaf": {
+ "rettype":"float",
+ "args": ["float","float","float"]
+ },
+ "__builtin_fmal": {
+ "rettype":"long double",
+ "args": ["long double","long double","long double"]
+ },
+ "__builtin_fmax": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_fmaxf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_fmaxl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_fmin": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_fminf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_fminl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_fmod": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_fmodf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_fmodl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_fprintf": {
+ "rettype":"int",
+ "args": ["void *","char const *"],
+ "variadic":true
+ },
+ "__builtin_fputs": {
+ "rettype":"int",
+ "args": ["char const *","void *"]
+ },
+ "__builtin_frame_address": {
+ "rettype":"void *",
+ "args": ["unsigned int"]
+ },
+ "__builtin_free": {
+ "rettype":"void",
+ "args": ["void *"]
+ },
+ "__builtin_frexp": {
+ "rettype":"double",
+ "args": ["double","int *"]
+ },
+ "__builtin_frexpf": {
+ "rettype":"float",
+ "args": ["float","int *"]
+ },
+ "__builtin_frexpl": {
+ "rettype":"long double",
+ "args": ["long double","int *"]
+ },
+ "__builtin_fscanf": {
+ "rettype":"int",
+ "args": ["void *","char const *"],
+ "variadic":true
+ },
+ "__builtin_huge_val": {
+ "rettype":"double",
+ "args": []
+ },
+ "__builtin_huge_valf": {
+ "rettype":"float",
+ "args": []
+ },
+ "__builtin_huge_vall": {
+ "rettype":"long double",
+ "args": []
+ },
+ "__builtin_hypot": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_hypotf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_hypotl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_ia32_lfence": {
+ "rettype":"void",
+ "args": []
+ },
+ "__builtin_ia32_mfence": {
+ "rettype":"void",
+ "args": []
+ },
+ "__builtin_ia32_sfence": {
+ "rettype":"void",
+ "args": []
+ },
+ "__builtin_ilogb": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_ilogbf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_ilogbl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_inf": {
+ "rettype":"double",
+ "args": []
+ },
+ "__builtin_inff": {
+ "rettype":"float",
+ "args": []
+ },
+ "__builtin_infl": {
+ "rettype":"long double",
+ "args": []
+ },
+ "__builtin_isalnum": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isalpha": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isblank": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_iscntrl": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isdigit": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isgraph": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_islower": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isprint": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_ispunct": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isspace": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isupper": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_isxdigit": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_labs": {
+ "rettype":"long",
+ "args": ["long"]
+ },
+ "__builtin_ldexp": {
+ "rettype":"double",
+ "args": ["double","int"]
+ },
+ "__builtin_ldexpf": {
+ "rettype":"float",
+ "args": ["float","int"]
+ },
+ "__builtin_ldexpl": {
+ "rettype":"long double",
+ "args": ["long double","int"]
+ },
+ "__builtin_lgamma": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_lgammaf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_lgammal": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_llabs": {
+ "rettype":"long long",
+ "args": ["long long"]
+ },
+ "__builtin_llrint": {
+ "rettype":"long long",
+ "args": ["double"]
+ },
+ "__builtin_llrintf": {
+ "rettype":"long long",
+ "args": ["float"]
+ },
+ "__builtin_llrintl": {
+ "rettype":"long long",
+ "args": ["long double"]
+ },
+ "__builtin_llround": {
+ "rettype":"long long",
+ "args": ["double"]
+ },
+ "__builtin_llroundf": {
+ "rettype":"long long",
+ "args": ["float"]
+ },
+ "__builtin_llroundl": {
+ "rettype":"long long",
+ "args": ["long double"]
+ },
+ "__builtin_log": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_log10": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_log10f": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_log10l": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_log1p": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_log1pf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_log1pl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_log2": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_log2f": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_log2l": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_logb": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_logbf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_logbl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_logf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_logl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_lrint": {
+ "rettype":"long",
+ "args": ["double"]
+ },
+ "__builtin_lrintf": {
+ "rettype":"long",
+ "args": ["float"]
+ },
+ "__builtin_lrintl": {
+ "rettype":"long",
+ "args": ["long double"]
+ },
+ "__builtin_lround": {
+ "rettype":"long",
+ "args": ["double"]
+ },
+ "__builtin_lroundf": {
+ "rettype":"long",
+ "args": ["float"]
+ },
+ "__builtin_lroundl": {
+ "rettype":"long",
+ "args": ["long double"]
+ },
+ "__builtin_malloc": {
+ "rettype":"void *",
+ "args": ["size_t"]
+ },
+ "__builtin_memchr": {
+ "rettype":"void *",
+ "args": ["void const *","int","size_t"]
+ },
+ "__builtin_memcmp": {
+ "rettype":"int",
+ "args": ["void const *","void const *","size_t"]
+ },
+ "__builtin_memcpy": {
+ "rettype":"void *",
+ "args": ["void *","void const *","size_t"]
+ },
+ "__builtin_mempcpy": {
+ "rettype":"void *",
+ "args": ["void *","void const *","size_t"]
+ },
+ "__builtin_memset": {
+ "rettype":"void *",
+ "args": ["void *","int","size_t"]
+ },
+ "__builtin_modf": {
+ "rettype":"double",
+ "args": ["double","double *"]
+ },
+ "__builtin_modff": {
+ "rettype":"float",
+ "args": ["float","float *"]
+ },
+ "__builtin_modfl": {
+ "rettype":"long double",
+ "args": ["long double","long double *"]
+ },
+ "__builtin_nan": {
+ "rettype":"double",
+ "args": ["char const *"]
+ },
+ "__builtin_nanf": {
+ "rettype":"float",
+ "args": ["char const *"]
+ },
+ "__builtin_nanl": {
+ "rettype":"long double",
+ "args": ["char const *"]
+ },
+ "__builtin_nans": {
+ "rettype":"double",
+ "args": ["char const *"]
+ },
+ "__builtin_nansf": {
+ "rettype":"float",
+ "args": ["char const *"]
+ },
+ "__builtin_nansl": {
+ "rettype":"long double",
+ "args": ["char const *"]
+ },
+ "__builtin_nearbyint": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_nearbyintf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_nearbyintl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_nextafter": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_nextafterf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_nextafterl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_nexttoward": {
+ "rettype":"double",
+ "args": ["double","long double"]
+ },
+ "__builtin_nexttowardf": {
+ "rettype":"float",
+ "args": ["float","long double"]
+ },
+ "__builtin_nexttowardl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_object_size": {
+ "rettype":"size_t",
+ "args": ["void *","int"]
+ },
+ "__builtin_offsetof": {
+ "rettype":"size_t",
+ "args": ["size_t"]
+ },
+ "__builtin_parity": {
+ "rettype":"int",
+ "args": ["unsigned int"]
+ },
+ "__builtin_parityl": {
+ "rettype":"int",
+ "args": ["unsigned long"]
+ },
+ "__builtin_parityll": {
+ "rettype":"int",
+ "args": ["unsigned long long"]
+ },
+ "__builtin_pow": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_powf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_powi": {
+ "rettype":"double",
+ "args": ["double","int"]
+ },
+ "__builtin_powif": {
+ "rettype":"float",
+ "args": ["float","int"]
+ },
+ "__builtin_powil": {
+ "rettype":"long double",
+ "args": ["long double","int"]
+ },
+ "__builtin_powl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_prefetch": {
+ "rettype":"void",
+ "args": ["void const *"],
+ "variadic":true
+ },
+ "__builtin_printf": {
+ "rettype":"int",
+ "args": ["char const *"],
+ "variadic":true
+ },
+ "__builtin_putchar": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_puts": {
+ "rettype":"int",
+ "args": ["char const *"]
+ },
+ "__builtin_realloc": {
+ "rettype":"void *",
+ "args": ["void *","size_t"]
+ },
+ "__builtin_remainder": {
+ "rettype":"double",
+ "args": ["double","double"]
+ },
+ "__builtin_remainderf": {
+ "rettype":"float",
+ "args": ["float","float"]
+ },
+ "__builtin_remainderl": {
+ "rettype":"long double",
+ "args": ["long double","long double"]
+ },
+ "__builtin_remquo": {
+ "rettype":"double",
+ "args": ["double","double","int *"]
+ },
+ "__builtin_remquof": {
+ "rettype":"float",
+ "args": ["float","float","int *"]
+ },
+ "__builtin_remquol": {
+ "rettype":"long double",
+ "args": ["long double","long double","int *"]
+ },
+ "__builtin_return": {
+ "rettype":"void",
+ "args": ["void const *"]
+ },
+ "__builtin_return_address": {
+ "rettype":"void *",
+ "args": ["unsigned int"]
+ },
+ "__builtin_rint": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_rintf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_rintl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_round": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_roundf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_roundl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_scalbln": {
+ "rettype":"double",
+ "args": ["double","long"]
+ },
+ "__builtin_scalblnf": {
+ "rettype":"float",
+ "args": ["float","long"]
+ },
+ "__builtin_scalblnl": {
+ "rettype":"long double",
+ "args": ["long double","long"]
+ },
+ "__builtin_scalbn": {
+ "rettype":"double",
+ "args": ["double","int"]
+ },
+ "__builtin_scalbnf": {
+ "rettype":"float",
+ "args": ["float","int"]
+ },
+ "__builtin_scalbnl": {
+ "rettype":"long double",
+ "args": ["long double","int"]
+ },
+ "__builtin_scanf": {
+ "rettype":"int",
+ "args": ["char const *"],
+ "variadic":true
+ },
+ "__builtin_sin": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_sinf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_sinh": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_sinhf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_sinhl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_sinl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_snprintf": {
+ "rettype":"int",
+ "args": ["char *","size_t","char const *"],
+ "variadic":true
+ },
+ "__builtin_sprintf": {
+ "rettype":"int",
+ "args": ["char *","char const *"],
+ "variadic":true
+ },
+ "__builtin_sqrt": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_sqrtf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_sqrtl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_sscanf": {
+ "rettype":"int",
+ "args": ["char const *","char const *"],
+ "variadic":true
+ },
+ "__builtin_stdarg_start": {
+ "rettype":"void",
+ "args": ["__builtin_va_list"]
+ },
+ "__builtin_stpcpy": {
+ "rettype":"char *",
+ "args": ["char *","char const *"]
+ },
+ "__builtin_strcat": {
+ "rettype":"char *",
+ "args": ["char *","char const *"]
+ },
+ "__builtin_strchr": {
+ "rettype":"char *",
+ "args": ["char *","int"]
+ },
+ "__builtin_strcmp": {
+ "rettype":"int",
+ "args": ["char const *","char const *"]
+ },
+ "__builtin_strcpy": {
+ "rettype":"char *",
+ "args": ["char *","char const *"]
+ },
+ "__builtin_strcspn": {
+ "rettype":"size_t",
+ "args": ["char const *","char const *"]
+ },
+ "__builtin_strlen": {
+ "rettype":"size_t",
+ "args": ["char const *"]
+ },
+ "__builtin_strncat": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t"]
+ },
+ "__builtin_strncmp": {
+ "rettype":"int",
+ "args": ["char const *","char const *","size_t"]
+ },
+ "__builtin_strncpy": {
+ "rettype":"char *",
+ "args": ["char *","char const *","size_t"]
+ },
+ "__builtin_strpbrk": {
+ "rettype":"char *",
+ "args": ["char const *","char const *"]
+ },
+ "__builtin_strrchr": {
+ "rettype":"char *",
+ "args": ["char const *","int"]
+ },
+ "__builtin_strspn": {
+ "rettype":"size_t",
+ "args": ["char const *","char const *"]
+ },
+ "__builtin_strstr": {
+ "rettype":"char *",
+ "args": ["char const *","char const *"]
+ },
+ "__builtin_tan": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_tanf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_tanh": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_tanhf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_tanhl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_tanl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_tgamma": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_tgammaf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_tgammal": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_tolower": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_toupper": {
+ "rettype":"int",
+ "args": ["int"]
+ },
+ "__builtin_trunc": {
+ "rettype":"double",
+ "args": ["double"]
+ },
+ "__builtin_truncf": {
+ "rettype":"float",
+ "args": ["float"]
+ },
+ "__builtin_truncl": {
+ "rettype":"long double",
+ "args": ["long double"]
+ },
+ "__builtin_types_compatible_p": {
+ "rettype":"int",
+ "args": ["size_t","size_t"]
+ },
+ "__builtin_unreachable": {
+ "rettype":"void",
+ "args": []
+ },
+ "__builtin_vfprintf": {
+ "rettype":"int",
+ "args": ["void *","char const *","__builtin_va_list"]
+ },
+ "__builtin_vfscanf": {
+ "rettype":"int",
+ "args": ["void *","char const *","__builtin_va_list"]
+ },
+ "__builtin_vprintf": {
+ "rettype":"int",
+ "args": ["char const *","__builtin_va_list"]
+ },
+ "__builtin_vscanf": {
+ "rettype":"int",
+ "args": ["char const *","__builtin_va_list"]
+ },
+ "__builtin_vsnprintf": {
+ "rettype":"int",
+ "args": ["char *","size_t","char const *","__builtin_va_list"]
+ },
+ "__builtin_vsprintf": {
+ "rettype":"int",
+ "args": ["char *","char const *","__builtin_va_list"]
+ },
+ "__builtin_vsscanf": {
+ "rettype":"int",
+ "args": ["char const *","char const *","__builtin_va_list"]
+ },
+ "__sync_add_and_fetch": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_and_and_fetch": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_bool_compare_and_swap": {
+ "rettype":"int",
+ "args": ["T volatile *", "T", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_fetch_and_add": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_fetch_and_and": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_fetch_and_nand": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_fetch_and_or": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_fetch_and_sub": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_fetch_and_xor": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_lock_release": {
+ "rettype":"void",
+ "args": ["T 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": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_nand_and_fetch": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_or_and_fetch": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_sub_and_fetch": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_val_compare_and_swap": {
+ "rettype":"T",
+ "args": ["T volatile *","T","T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ },
+ "__sync_xor_and_fetch": {
+ "rettype":"T",
+ "args": ["T volatile *", "T"],
+ "types":["int8_t", "int16_t", "int32_t", "int64_t", "uint8_t", "uint16_t", "uint32_t", "uint64_t"],
+ "variadic":true
+ }
+ }
+}
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 0363e6ffa8aa2cf372c856c446b81edac0630a94..95cd3898f7e219c8f942cc710317e1c7300f2166 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -246,14 +246,31 @@ let () = Cmdline.run_after_exiting_stage run_list_all_plugin_options
(* Hooks independent from cmdline ordering *)
(**************************************************************************)
+let warn_if_another_compiler_builtin name =
+ try
+ (* Before warning, we must make sure the builtins from other compilers
+ are loaded. *)
+ if not (Cil_builtins.Gcc_builtin_templates_loaded.get ()) then
+ Cil_builtins.init_gcc_builtin_templates ();
+ let bt = Cil_builtins.Builtin_templates.find name in
+ let compiler = Option.get bt.compiler in
+ Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
+ ~current:true ~once:true
+ "%s is a compiler builtin, %s" name
+ (Cil.allowed_machdep (Cil_builtins.string_of_compiler compiler));
+ true
+ with Not_found -> false
+
(* This hook cannot be registered directly in Kernel or Cabs2cil, as it
depends on Ast_info *)
let on_call_to_undeclared_function vi =
let name = vi.Cil_types.vname in
- if not (Ast_info.is_frama_c_builtin name) then
- Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
- ~current:true ~once:true
- "Calling undeclared function %s. Old style K&R code?" name
+ if not (Ast_info.is_frama_c_builtin name) then begin
+ if not (warn_if_another_compiler_builtin name) then
+ Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
+ ~current:true ~once:true
+ "Calling undeclared function %s. Old style K&R code?" name
+ end
let () =
Cabs2cil.register_implicit_prototype_hook on_call_to_undeclared_function
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index ca1847c257adda363197d1c5bf583f2eee49073f..d7a95024779daa31e2a2c069307f9f3818b672b1 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1223,8 +1223,12 @@ class cil_printer () = object (self)
| Some vi ->
let formals = Cil.getFormalsDecl vi in
match List.rev formals with
- | [] -> assert false (* Typing error, this function is variadic and should
- have at least one argument *)
+ | [] ->
+ (* Typing error, this function should
+ have at least one named argument *)
+ Kernel.abort ~current:true
+ "%s should have at least one named argument"
+ vi.vname
| f :: _ -> Cil.new_exp ~loc:f.vdecl (Lval (Cil.var f))
(**** STATEMENTS ****)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index bdf9ad830c3992722787f154cb9b959a18e87840..43579c3d1661338d015733e3e3ce843268992ed4 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -171,8 +171,8 @@ let acceptEmptyCompinfo () =
let allowed_machdep machdep =
Format.asprintf
- "only allowed for %s machdeps;@ see option -machdep or@ \
- run '-machdep help' for the list of available machdeps"
+ "only allowed for %s machdeps; see option -machdep or \
+ run 'frama-c -machdep help' for the list of available machdeps"
machdep
let theMachineProject = ref (createMachine ())
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index b990e16a029101eeb3a1762514523a6ba30e7914..4d0545f91f3f05c0e4251f395a25a5748f373bbe 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -100,484 +100,154 @@ 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)
+module Gcc_builtin_templates_loaded =
+ State_builder.Ref
+ (Datatype.Bool)
+ (struct
+ let name = "Cil_builtins.Gcc_builtin_templates_loaded"
+ let dependencies = [ Builtin_templates.self ]
+ let default () = false
+ 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 ?default_compiler fp =
+ let json = parse fp in
+ List.iter (fun (name, entry) ->
+ let compiler =
+ if default_compiler <> None then default_compiler
+ else
+ 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_option |> Option.is_some
+ 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.
+ Note that the type strings must follow a strict format (also used
+ in gcc_builtins.json), with a single space between type names and
+ asterisks (for pointers); otherwise we would have to do some expensive
+ matching.
+*)
+let build_type_table () : (string, typ option) Hashtbl.t =
let int8_t = Some Cil.scharType in
let int16_t = try Some (Cil.int16_t ()) with Not_found -> None in
let int32_t = try Some (Cil.int32_t ()) with Not_found -> None in
@@ -586,126 +256,169 @@ 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
+ 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)
+
+(* Note that [s] (the type string) follows a stricter format than the ones
+ allowed by the C standard w.r.t. type names; a single space must be
+ present between type names and asterisks. *)
+let parse_type ?(template="") type_table s =
+ try
+ if String.get s 0 == 'T' then
+ (* replace 'T' (always at the beginning) with the template *)
+ let typ = template ^ (String.sub s 1 (String.length s - 1)) 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
+
+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
- (* 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"]
+(* 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
- let add_sync (typ,name) f =
- match typ with
- | Some typ ->
- add ~prefix:"__sync_" (f^name) typ [ TPtr(typeAddVolatile typ,[]); typ] true
- | None -> ()
+ 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 init_gcc_builtin_templates () =
+ let fp =
+ Datatype.Filepath.concat ~existence:Filepath.Must_exist
+ Fc_config.datadir "compliance/gcc_builtins.json"
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;
- end
+ Json.init_builtin_templates ~default_compiler:GCC fp;
+ Gcc_builtin_templates_loaded.set true
-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
-
-let register_custom_builtin (name, rt, prms, isva) =
- Builtin_functions.add name (rt,prms,isva)
+let init_other_builtin_templates () =
+ let fp =
+ Datatype.Filepath.concat ~existence:Filepath.Must_exist
+ Fc_config.datadir "compliance/compiler_builtins.json"
+ in
+ Json.init_builtin_templates fp
+
+let init_builtins_from_json () =
+ (* For performance reasons, we avoid loading GCC builtins unless we are
+ using a GCC machdep *)
+ if Cil.gccMode () then init_gcc_builtin_templates ();
+ init_other_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_from_json ();
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 3c08e8507bcfa5c0cf69869f7b19d4ff4575eba2..ebbebbbde4dfe3bb30cb2f4f8eb59d258aafbc16 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -95,6 +95,27 @@ 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
+
+module Gcc_builtin_templates_loaded : State_builder.Ref with type data = bool
+
+val init_gcc_builtin_templates : unit -> unit
+
(** 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 9b4ae61a64246bc9d7aefa81625d64de917c09b3..79d3b8c13ee0971dcb5998151e3518a3ed9e62bf 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 8c74bc0b8673d5e28856e00545395b1a00151c48..aa8edb92053a3a009ba32c0039308314e88e52da 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 c9e5ac23e74804d60a2ce769d98841a80b8f1ce0..cce5ee0c72fd8bfff0f6616323d476924a45e012 100644
--- a/tests/compliance/check-json.i
+++ b/tests/compliance/check-json.i
@@ -1,9 +1,11 @@
/*run.config
MACRO: SHARE @FRAMAC_SHARE@/compliance
NOFRAMAC:
- EXECNOW: LOG json_@PTEST_NAME@_1.txt python3 -m json.tool < @SHARE@/c11_functions.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_1.txt 2> @DEV_NULL@
- 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@_1.txt python3 -m json.tool < @SHARE@/c11_functions.json | head -n 2 | tail -n 1 > @PTEST_RESULT@/json_@PTEST_NAME@_1.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_2.txt python3 -m json.tool < @SHARE@/glibc_functions.json | head -n 2 | tail -n 1 > @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 | tail -n 1 > @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 | tail -n 1 > @PTEST_RESULT@/json_@PTEST_NAME@_4.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_5.txt python3 -m json.tool < @SHARE@/compiler_builtins.json | head -n 2 | tail -n 1 > @PTEST_RESULT@/json_@PTEST_NAME@_5.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_6.txt python3 -m json.tool < @SHARE@/gcc_builtins.json | head -n 2 | tail -n 1 > @PTEST_RESULT@/json_@PTEST_NAME@_6.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_7.txt python3 @PTEST_DIR@/sanity-checks.py @SHARE@ > @PTEST_RESULT@/json_@PTEST_NAME@_7.txt 2> @DEV_NULL@
*/
diff --git a/tests/compliance/oracle/json_check-json_1.txt b/tests/compliance/oracle/json_check-json_1.txt
index 1b5870264ab3d7511f6c0ec3cce36b2ddf76554c..53e785991f5381a46f4610e816316649ccae7e5e 100644
--- a/tests/compliance/oracle/json_check-json_1.txt
+++ b/tests/compliance/oracle/json_check-json_1.txt
@@ -1,2 +1 @@
-{
"description": "C11 reserved function and macro identifiers",
diff --git a/tests/compliance/oracle/json_check-json_2.txt b/tests/compliance/oracle/json_check-json_2.txt
index a7490e8d444cf0359541826585e85c435704ea3e..24ce34e11953f9c80a6861f91fcfc97fe6f70171 100644
--- a/tests/compliance/oracle/json_check-json_2.txt
+++ b/tests/compliance/oracle/json_check-json_2.txt
@@ -1,2 +1 @@
-{
"description": "Function and macro identifiers defined in the GNU C Library",
diff --git a/tests/compliance/oracle/json_check-json_3.txt b/tests/compliance/oracle/json_check-json_3.txt
index 0b2f8f38fd6866c709dd788271b9c62fe2a52bf0..567fa7bd16e3060df956746d155eb99beecf0acf 100644
--- a/tests/compliance/oracle/json_check-json_3.txt
+++ b/tests/compliance/oracle/json_check-json_3.txt
@@ -1,2 +1 @@
-{
"description": "Non-ISO C, Non-POSIX identifiers known to the Frama-C standard library",
diff --git a/tests/compliance/oracle/json_check-json_4.txt b/tests/compliance/oracle/json_check-json_4.txt
index cdf3ccde431a21b0e3e97353e314452444a135a1..ba1f81a5fad309e92a7b2db78855d59bd595be79 100644
--- a/tests/compliance/oracle/json_check-json_4.txt
+++ b/tests/compliance/oracle/json_check-json_4.txt
@@ -1,2 +1 @@
-{
"description": "POSIX.1-2008 reserved function identifiers (plus a few legacy POSIX identifiers)",
diff --git a/tests/compliance/oracle/json_check-json_5.txt b/tests/compliance/oracle/json_check-json_5.txt
index 295b7a131d220022bb1905180900314974130baa..41629175862962f64941c7ec80ef2948a41e695a 100644
--- a/tests/compliance/oracle/json_check-json_5.txt
+++ b/tests/compliance/oracle/json_check-json_5.txt
@@ -1,2 +1 @@
-posix_identifiers.json checked.
-c11_functions.json checked.
+ "description": "Compiler builtins supported by Frama-C (for GCC builtins, see gcc_builtins.json)",
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 0000000000000000000000000000000000000000..6984653217284e726bb24afefc98bf10d49420a2
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_6.txt
@@ -0,0 +1 @@
+ "description": "GCC builtins supported by Frama-C",
diff --git a/tests/compliance/oracle/json_check-json_7.txt b/tests/compliance/oracle/json_check-json_7.txt
new file mode 100644
index 0000000000000000000000000000000000000000..295b7a131d220022bb1905180900314974130baa
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_7.txt
@@ -0,0 +1,2 @@
+posix_identifiers.json checked.
+c11_functions.json checked.
diff --git a/tests/misc/oracle/function_ptr_alignof.res.oracle b/tests/misc/oracle/function_ptr_alignof.res.oracle
index fa223563fb4e588997e95f7fee1b314ec2c92b0e..c25dcf5f2d7b15f305cca1a86fb38435120a3078 100644
--- a/tests/misc/oracle/function_ptr_alignof.res.oracle
+++ b/tests/misc/oracle/function_ptr_alignof.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing function_ptr_alignof.i (no preprocessing)
[kernel] function_ptr_alignof.i:13: User Error:
- alignof() called on function only allowed for GCC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ alignof() called on function only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "function_ptr_alignof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_sizeof.res.oracle b/tests/misc/oracle/function_ptr_sizeof.res.oracle
index 06996432c675f999cba76b50b0b13b2e72083267..3f66d533ba61c68d95e83705e0ba3ca5ad41afc3 100644
--- a/tests/misc/oracle/function_ptr_sizeof.res.oracle
+++ b/tests/misc/oracle/function_ptr_sizeof.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing function_ptr_sizeof.i (no preprocessing)
[kernel] function_ptr_sizeof.i:13: User Error:
- sizeof() called on function only allowed for GCC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ sizeof() called on function only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "function_ptr_sizeof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/compiler_builtins.c b/tests/syntax/compiler_builtins.c
new file mode 100644
index 0000000000000000000000000000000000000000..175483a73c1cc5eea357932151b7e59e0e79d7d4
--- /dev/null
+++ b/tests/syntax/compiler_builtins.c
@@ -0,0 +1,28 @@
+/* run.config
+ STDOPT:
+ STDOPT: +"-machdep gcc_x86_32"
+ STDOPT: +"-machdep msvc_x86_64"
+ */
+
+#include <stdarg.h>
+
+struct st {
+ char a;
+ int b;
+};
+
+void fva(int a, ...) {
+ va_list ap;
+ __builtin_va_start(ap, a); // Non-MSVC-specific
+ __builtin_va_end(ap); // Non-MSVC-specific
+}
+
+int main() {
+ int x = 0;
+ if (__builtin_expect(x++, x)) { // GCC-specific
+ int y = x;
+ }
+ __builtin__annotation("a", 1); // MSVC-specific
+ fva(1);
+ __builtin_offsetof(struct st,b); // Generic builtin (always available)
+}
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 32d925b4bfe4c3c97c19d67815d1f978afa4b0b1..d115b107f7d2ae95a82989316364464b299d9ba3 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);
diff --git a/tests/syntax/oracle/compiler_builtins.0.res.oracle b/tests/syntax/oracle/compiler_builtins.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..962db45f53cb5561a0deb60970e2613d548793c1
--- /dev/null
+++ b/tests/syntax/oracle/compiler_builtins.0.res.oracle
@@ -0,0 +1,41 @@
+[kernel] Parsing compiler_builtins.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:22: Warning:
+ __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:25: Warning:
+ __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+/* Generated by Frama-C */
+#include "stdarg.h"
+/* compiler builtin:
+ void __builtin_va_end(__builtin_va_list); */
+/* compiler builtin:
+ void __builtin_va_start(__builtin_va_list); */
+void fva(int a , ...)
+{
+ va_list ap;
+ __builtin_va_start(ap,a);
+ __builtin_va_end(ap);
+ return;
+}
+
+extern int ( /* missing proto */ __builtin__annotation)(char const *x_0,
+ int x_1);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int x = 0;
+ ;
+ tmp = x;
+ x ++;
+ ;
+ if (tmp) {
+ int y = x;
+ }
+ __builtin__annotation("a",1);
+ fva(1);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/compiler_builtins.1.res.oracle b/tests/syntax/oracle/compiler_builtins.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d3cf8ba1bb5ad1cc0fe1cdac0ccb120a283ab22d
--- /dev/null
+++ b/tests/syntax/oracle/compiler_builtins.1.res.oracle
@@ -0,0 +1,39 @@
+[kernel] Parsing compiler_builtins.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:25: Warning:
+ __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+/* Generated by Frama-C */
+#include "stdarg.h"
+/* compiler builtin:
+ void __builtin_va_end(__builtin_va_list); */
+/* compiler builtin:
+ void __builtin_va_start(__builtin_va_list); */
+void fva(int a , ...)
+{
+ va_list ap;
+ __builtin_va_start(ap,a);
+ __builtin_va_end(ap);
+ return;
+}
+
+extern int ( /* missing proto */ __builtin__annotation)(char const *x_0,
+ int x_1);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int x = 0;
+ ;
+ tmp = x;
+ x ++;
+ ;
+ if ((long)tmp) {
+ int y = x;
+ }
+ __builtin__annotation("a",1);
+ fva(1);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/compiler_builtins.2.res.oracle b/tests/syntax/oracle/compiler_builtins.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cc838d9c9cda183f69fbda4630ecf2522fd5f223
--- /dev/null
+++ b/tests/syntax/oracle/compiler_builtins.2.res.oracle
@@ -0,0 +1,42 @@
+[kernel] Parsing compiler_builtins.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:16: Warning:
+ __builtin_va_start is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:17: Warning:
+ __builtin_va_end is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:22: Warning:
+ __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+/* Generated by Frama-C */
+#include "stdarg.h"
+/* compiler builtin:
+ void __builtin__annotation(...); */
+extern int ( /* missing proto */ __builtin_va_start)();
+
+extern int ( /* missing proto */ __builtin_va_end)(char *x_0);
+
+void fva(int a , ...)
+{
+ va_list ap;
+ __builtin_va_start(ap,a);
+ __builtin_va_end(ap);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int x = 0;
+ ;
+ tmp = x;
+ x ++;
+ ;
+ if (tmp) {
+ int y = x;
+ }
+ __builtin__annotation("a",1);
+ fva(1);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
index 8f91488188b6cb3016ee725eb2f25ea96c38bd2f..22cf6e91dadcdb16d2f811aa88e9247b8b4730c4 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing flexible_array_member_invalid5.i (no preprocessing)
[kernel] flexible_array_member_invalid5.i:15: User Error:
- field `f' declared with a type containing a flexible array member only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps.
+ field `f' declared with a type containing a flexible array member only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps.
[kernel] User Error: stopping on file "flexible_array_member_invalid5.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/sizeof_void.0.res.oracle b/tests/syntax/oracle/sizeof_void.0.res.oracle
index 03f35c1ead217d855a3261324725e1624285c621..9ad43d07487edb653606707fc19113361b096509 100644
--- a/tests/syntax/oracle/sizeof_void.0.res.oracle
+++ b/tests/syntax/oracle/sizeof_void.0.res.oracle
@@ -1,16 +1,12 @@
[kernel] Parsing sizeof_void.c (with preprocessing)
[kernel] sizeof_void.c:9: User Error:
- sizeof on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ sizeof on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] sizeof_void.c:16: User Error:
- sizeof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ sizeof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] sizeof_void.c:21: User Error:
- alignof on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ alignof on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] sizeof_void.c:28: User Error:
- alignof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ alignof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "sizeof_void.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index 985351e9ac4efd6f3aef9393e0a6980017dfc493..5ed5a2552d7bdc8bf214e134b0f66d1bb4b00e55 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -1,16 +1,13 @@
[kernel] Parsing array_zero_length.i (no preprocessing)
[kernel] array_zero_length.i:9: User Error:
- zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] array_zero_length.i:11: User Error:
- zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] array_zero_length.i:11: User Error:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are not allowed in C99
[kernel] array_zero_length.i:13: User Error:
- empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
11 char W[][0];
12
13 char T1[] = {};
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index 446b635cc2cd1897e645b94688a5ece3a0e6bc81..019c09a82d65b2fb085b5c5523accd75088742c0 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,13 +1,10 @@
[kernel] Parsing empty_base.c (with preprocessing)
[kernel] empty_base.c:13: User Error:
- empty structs only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ empty structs only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] empty_base.c:48: User Error:
- zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] empty_base.c:50: User Error:
- empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
48 struct empty empty_array_of_empty[0];
49 struct empty array_of_empty[1];
50 struct empty many_empty[3] = {{}};