--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2018 ---
Hi everyone, we are currently studying the usage of GCC builtins [1] by GitHub projects and how well various tools support them. To that end, we are also developing a test suite for the most frequently used machine-independent GCC builtins (available at https://github.com/gcc-builtins/tests). We'd be glad to contribute the test suite (or parts of it) to Frama-C, if you are interested. >From the test cases, it seems that Frama-C does not support any of the most-frequently-used public builtins. It appears that they are not recognized, as I get warnings like this one: "Warning: Calling undeclared function __builtin_expect. Old style K&R code?" >From the source code (in src/kernel_internals/typing/cabs2cil.ml), it seems that the GCC-internal builtins for varargs handling (e.g., __builtin_va_start, __builtin_va_arg, and __builtin_va_end) are supported, which I verified with an additional test case. Besides, I found some evidence in the code that __builtin_compatible_p is supported (which is also mentioned in the changelog: "Support for static evaluation of the __builtin_compatible_p GCC specific function."). Nevertheless, Frama-C does not seem to actually support that builtin. The same is true for some other builtins (like __builtin_constant_p and __builtin_expect). Are there any plans to support more GCC builtins in Frama-C or does a Frama-C plugin already support them? Some of the frequently used builtins have equivalent libc functions (e.g., __builtin_fabs is equivalent to fabs). To me, defining aliases to the libc equivalents would seem like a first step to add better builtin support to Frama-C. Best, Manuel [1] https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180712/32341708/attachment.html>