Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] GCC Builtins Support

  • Subject: [Frama-c-discuss] GCC Builtins Support
  • From: rigger.manuel at gmail.com (Manuel Rigger)
  • Date: Thu, 12 Jul 2018 14:18:37 +0200
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>