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

Thanks for the reports, we will take a look at the issues. INFINITY and 
NAN are indeed missing from our libc and will be added. About the other 
remarks, we'll take a look and see what needs to be changed, and come 
back to you later.


On 17/07/18 16:27, Manuel Rigger wrote:
> 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 	 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
> _______________________________________________
> 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 --------------
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/20180718/73b4f8cf/attachment-0001.bin>