search

goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

Add missing `_builtin`s #69

Open michael-schwarz opened 2 years ago

michael-schwarz commented 2 years ago

Some __builitns were identiefied as missing during https://github.com/goblint/analyzer/pull/528. These should be added to CIL.

sim642 commented 11 months ago

The Concrat benchmarks were merged with Goblint CIL 1.8.2 and contain some builtin declarations with missing prototypes:

I thought I'd just add them, but it's not so easy it seems. https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html doesn't specify them with argument types, just as behaving like the C standard ones. But the C standard versions aren't functions but macros. This is because the same function has to work for float, double and long double without the function being suffixed. This might even be the reason why these builtins haven't been specified a long time ago in CIL.

Clang internally has its own special Floating type to represent it: https://github.com/llvm/llvm-project/blob/ce9077fe7f0ceb2800076aa1abb472de5df41f16/clang/lib/AST/Interp/InterpBuiltin.cpp#L294-L296.