--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on July 2018 ---
Hello André, thanks a lot for your response! With this option, 41 of the 100 test cases do not result in a warning or error. In 35 cases, builtins are still not recognized. In 9 cases, Frama-C aborts because the INFINITY or NAN macro are used. Is there some way to define them over compiler flags? 14 test cases fail due to type mismatches in the __sync builtins. For example, for the __sync_add_and_fetch test case I get the error below: [kernel] Parsing test-cases/12-__sync_add_and_fetch.c (with preprocessing) [kernel:typing:incompatible-types-call] test-cases/12-__sync_add_and_fetch.c:5: Warning: expected 'int *' but got argument of type 'int volatile *': & a [kernel:typing:incompatible-types-call] test-cases/12-__sync_add_and_fetch.c:12: Warning: expected 'int *' but got argument of type 'long volatile *': & a [kernel:typing:incompatible-types-call] test-cases/12-__sync_add_and_fetch.c:19: Warning: expected 'long long *' but got argument of type 'long long volatile *': & a It seems that Frama-C does not expect volatile variables as input. Furthermore, the warning in line 12 is surprising. It can be reproduced with this simplified test case: #include <assert.h> void test_long() { long a = 1; long result = __sync_add_and_fetch(&a, 5L); assert(a == 6); assert(result == 6); } Frama-C expects `a` to be an int instead of a long variable, which is in conflict with the GCC docs (see https://gcc.gnu.org/onlinedocs/gcc-4.5.4/gcc/Atomic-Builtins.html). The versions for int and long long variables work as expected. Similar warnings are also emitted for __sync_fetch_and_xor, __sync_val_compare_and_swap, __sync_fetch_and_sub, __sync_fetch_and_add, __sync_fetch_and_and, __sync_and_and_fetch, __sync_fetch_and_and, __sync_or_and_fetch, __sync_fetch_and_or, __sync_bool_compare_and_swap, __sync_lock_test_and_set, __sync_lock_release, and __sync_sub_and_fetch. Is this a bug? I also stumbled over a second unexpected warning for __builtin_object_size. The reduced test case looks as follows: #include <assert.h> #include <stdlib.h> void local_buffer() { int var; size_t size = __builtin_object_size(&var, 0); assert(size == sizeof(int) || size == (size_t)-1); } The warning that I get is this: "[kernel] test.c:6: Failure: Cannot resolve variable ptr" Since there is no `ptr` variable in the test case, I assume that __builtin_object_size is implemented in terms of a macro that uses this undeclared variable? Best, Manuel 2018-07-17 15:05 GMT+02:00 Andre Maroneze <Andre.OLIVEIRAMARONEZE at cea.fr>: > 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), 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss