Skip to content

Fix GCC 16 warning-as-error build failures#9024

Open
StudyingFather wants to merge 4 commits into
diffblue:developfrom
StudyingFather:g++16-warning-fix
Open

Fix GCC 16 warning-as-error build failures#9024
StudyingFather wants to merge 4 commits into
diffblue:developfrom
StudyingFather:g++16-warning-fix

Conversation

@StudyingFather
Copy link
Copy Markdown

This PR fixes GCC 16 build failures caused by warnings promoted to errors (fixes #9004).

The changes cover four warning categories:

  • Avoid GCC 16 -Warray-bounds false positives involving ranget::map, json_stringt, and std::shared_ptr<std::function<...>> by using more direct JSON array construction in the affected paths.
  • Avoid GCC 16 -Warray-bounds false positives where virtual-call inlining/devirtualization appears to reason about a base object using a derived object layout.
  • Avoid -Wsfinae-incomplete by storing struct_encodingt's namespace as a plain reference instead of std::reference_wrapper<const namespacet> while namespacet is still incomplete.
  • Remove an actually unused SMT2 struct component counter reported by -Wunused-but-set-variable.

The intended behaviour is unchanged; these are either warning-path cleanups or removal of dead bookkeeping.

  • 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.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • 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.

GCC 16 reports false-positive -Warray-bounds warnings through the ranget::map shared_ptr/std::function instantiations used with json_stringt values.

Build the source-location pragma JSON array explicitly, and keep json_arrayt range-construction coverage by collecting an existing range of json_stringt values directly. This avoids the warning path without changing the JSON output or tested behaviour.
… dispatch

GCC 16 can report false-positive -Warray-bounds warnings after devirtualising and inlining calls on base-class objects as if derived-class layouts were available.

Call the known base implementations explicitly in the variable-sensitivity factory and the corresponding unit-test helper. The constructed dynamic types are unchanged, and the explicit calls avoid the over-eager diagnostic path.
GCC 16 warns when std::reference_wrapper<const namespacet> is instantiated while namespacet is still incomplete in struct_encoding.h.

Use a plain reference member instead. struct_encodingt already binds to an external namespace for its lifetime, so this preserves behaviour while avoiding -Wsfinae-incomplete under -Werror.
The counter in smt2_convt::unflatten was incremented while converting datatype structs but was never read.

Remove it, and keep the touched loop formatted, to avoid the GCC 16 -Wunused-but-set-variable warning under -Werror without changing the generated SMT2 output.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Compilation error with GCC 16.1.1 due to SFINAE warning.

1 participant