Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add missing _builtins #69

Open
michael-schwarz opened this issue Jan 19, 2022 · 1 comment
Open

Add missing _builtins #69

michael-schwarz opened this issue Jan 19, 2022 · 1 comment
Assignees
Labels

Comments

@michael-schwarz
Copy link
Member

Some __builitns were identiefied as missing during goblint/analyzer#528. These should be added to CIL.

@sim642
Copy link
Member

sim642 commented Oct 10, 2023

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

  • __builtin_isnan
  • __builtin_isinf_sign
  • __builtin_signbit

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants