Move and cleanup declarations of C compiler intrinsics

[tautschnig]

Please review commit-by-commit: the main added value is a new script that fetches Clang's declarations. The remaining commits are cleanup to facilitate easier updates of these intrinsics in future.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[NlightNFotis]

Sorry, question here because I cannot put it into a comment on the code (doesn't seem appropriate).

This appears to be adding a python script to print the compiler intrinsics from clang. It also mentions (on one of the commit messages) that this is supposed to substitute for an older script, but I don't see the older one being deleted anywhere.

Is this a mistake, or are both supposed to be used? Or is my understanding of the situation wrong?

[tautschnig]

Sorry, question here because I cannot put it into a comment on the code (doesn't seem appropriate).

This appears to be adding a python script to print the compiler intrinsics from clang. It also mentions (on one of the commit messages) that this is supposed to substitute for an older script, but I don't see the older one being deleted anywhere.

Is this a mistake, or are both supposed to be used? Or is my understanding of the situation wrong?

My apologies, I'll try to clarify the commit message: it's not really a substitute as the existing (bash) script fetches declarations from GCC's repository, while the new Python script fetches Clang's declarations. These declarations overlap to a great extent, but aren't completely the same. That said, however, the GCC script is rather brittle. Perhaps removing that script actually is the right thing to do. For now I'll just amend the commit message, but we might consider removing the bash script.

[codecov]

Codecov Report

Base: 78.34% // Head: 78.34% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (371d886) compared to base (a53fa0f).
Patch coverage: 93.33% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #6707   +/-   ##
========================================
  Coverage    78.34%   78.34%           
========================================
  Files         1644     1645    +1     
  Lines       190313   190358   +45     
========================================
+ Hits        149097   149133   +36     
- Misses       41216    41225    +9     

Impacted Files	Coverage Δ
jbmc/src/janalyzer/janalyzer_parse_options.cpp	48.58% <ø> (ø)
.../src/java_bytecode/character_refine_preprocess.cpp	54.27% <ø> (ø)
...mc/src/java_bytecode/character_refine_preprocess.h	100.00% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods.h	100.00% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp	98.41% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods_needed.h	100.00% <ø> (ø)
jbmc/src/java_bytecode/code_with_references.cpp	84.61% <ø> (ø)
jbmc/src/java_bytecode/java_bmc_util.cpp	100.00% <ø> (ø)
...mc/src/java_bytecode/java_bytecode_convert_class.h	0.00% <ø> (ø)
...src/java_bytecode/java_bytecode_convert_method.cpp	97.69% <ø> (ø)
... and 403 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[TGWDB]

I'm approving with the following caveats:

1. Adding a new script seems philosophically dangerous, now we have multiple places to gather the data we need
2. I don't think any of this is (well?) tested...
3. While it looks ok to me, I'm not really an expect in the compiler intrinsics area

[tautschnig]

I'm approving with the following caveats:

1. Adding a new script seems philosophically dangerous, now we have multiple places to gather the data we need

2. I don't think any of this is (well?) tested...

3. While it looks ok to me, I'm not really an expect in the compiler intrinsics area

Points taken. Maybe we can one day try to come up with a better story for compiler intrinsics. At the moment, this certainly is just a best-effort and not very organised activity.