--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on July 2018 ---
Hello, Thanks for the interest in Frama-C. By default, Frama-C assumes the input source code to be as close to the C standard as possible, which excludes compiler builtins in the name of portability. That said, usage of GCC-based architecture configuration files (called "machdeps", which include both machine features such as register size, but also compiler extensions, such as GCC and MSVC), e.g. with option `-machdep gcc_x86_32`, should enable some GCC builtins to be recognized. For instance, if I run `frama-c tests/syntax/gcc_builtins.c` (using the test files distributed in the Frama-C .tar.gz), I get: [kernel] Parsing tests/syntax/gcc_builtins.c (with preprocessing) [kernel:typing:implicit-function-declaration] tests/syntax/gcc_builtins.c:187: Warning:  Calling undeclared function __builtin_expect. Old style K&R code? However, if I add a GCC machdep, with `frama-c -machdep gcc_x86_32 tests/syntax/gcc_builtins.c`, the warning disappears: [kernel] Parsing tests/syntax/gcc_builtins.c (with preprocessing) Option `-machdep help` lists the available machdeps. Those prefixed with `gcc` enable GCC-specific features. Note that variadic functions, by default, are handled using the Variadic plug-in, so __builtin_va_start and similar ones may end up being translated by the plug-in after parsing. If you want to disable it, you'll need option `-variadic-no-translation`. Adding extra built-ins is usually done when needed for a case study; ideally, if there are interesting pieces of code using those builtins, we add them to be able to handle the code. Still, if all that is required is to add some macros, and there are already unit tests to check them, it could be worthwhile to add more built-ins. On 12/07/18 14:18, Manuel Rigger wrote: > 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 > <http://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 > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Researcher/Engineer CEA/LIST Software Reliability and Security Laboratory -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180717/e05b2c6d/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180717/e05b2c6d/attachment-0001.bin>