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

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>