Split goto_check

[kroening]

goto_check inserts assertions that check for suspect bugs in both C/C++ and
Java programs. The criteria differ vastly given that Java has basically no
instances of undefined behavior.

This PR splits the file, separating it into a checker for C/C++ and one
for Java. The long-term plan is to move these checkers into the directory
of the corresponding language frontend.

• Each commit message has a non-empty body, explaining why the change was made.
• 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).
• n/a My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6497 (9055c77) into develop (f245b3a) will increase coverage by 0.01%.
The diff coverage is 71.96%.

❗ Current head 9055c77 differs from pull request most recent head e286cd2. Consider uploading reports for the commit e286cd2 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6497      +/-   ##
===========================================
+ Coverage    76.06%   76.07%   +0.01%     
===========================================
  Files         1546     1548       +2     
  Lines       165584   166359     +775     
===========================================
+ Hits        125951   126563     +612     
- Misses       39633    39796     +163     

Impacted Files	Coverage Δ
...java_bytecode/java_bytecode_internal_additions.cpp	100.00% <ø> (ø)
jbmc/src/jdiff/jdiff_parse_options.h	100.00% <ø> (ø)
src/analyses/escape_analysis.cpp	63.83% <ø> (ø)
src/ansi-c/ansi_c_internal_additions.cpp	90.36% <ø> (ø)
src/ansi-c/c_typecheck_base.h	100.00% <ø> (ø)
src/crangler/ctokenit.cpp	0.00% <0.00%> (ø)
src/crangler/ctokenit.h	0.00% <0.00%> (ø)
src/goto-diff/goto_diff_parse_options.cpp	59.04% <ø> (+0.16%)	⬆️
src/goto-diff/goto_diff_parse_options.h	100.00% <ø> (ø)
src/goto-instrument/contracts/assigns.h	100.00% <ø> (ø)
... and 133 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d42839d...e286cd2. Read the comment docs.

[tautschnig]

I'm fine with that, but I note that we have several other PRs in flight that also affect this code. We need to co-ordinate at least with:

• Make pointer-primitive-check a no-op when behaviour is always defined #6491
• Prevent multiple instrumentation of a same check and instrumentation of instrumentation assertions #6471
• __CPROVER_r/w_ok does not require null or a valid pointer #6416
• Allow checks to be performed inside quantifier statements. #6399

[peterschrammel]

Looks like a reasonable intermediate step.

[kroening]

I'm fine with that, but I note that we have several other PRs in flight that also affect this code. We need to co-ordinate at least with:

• Make pointer-primitive-check a no-op when behaviour is always defined #6491
• Prevent multiple instrumentation of a same check and instrumentation of instrumentation assertions #6471
• __CPROVER_r/w_ok does not require null or a valid pointer #6416
• Allow checks to be performed inside quantifier statements. #6399

These all affect the checks for C, and should rebase easily since this PR renames goto_check.cpp to goto_check_c.cpp.

[tautschnig]

These all affect the checks for C, and should rebase easily since this PR renames goto_check.cpp to goto_check_c.cpp.

I'll try that on mine, but the mix of file renaming and clang-formatting could still spell trouble.

[tautschnig]

These all affect the checks for C, and should rebase easily since this PR renames goto_check.cpp to goto_check_c.cpp.

I'll try that on mine, but the mix of file renaming and clang-formatting could still spell trouble.

Add the renaming of the class into the mix. So, no, unfortunately it's not exactly fun. I've taken care of #6491, and will work with @remi-delmas-3000 on #6471.