--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] GCC Builtins Support



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>