--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on July 2018 ---
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>