Fix crash in shadow memory operations with zero-sized types

[tautschnig]

• Add ZST width checks in compute_or_over_bytes and compute_max_over_bytes
• Skip zero-sized components to prevent bitvector invariant violations
• Return default value (zero) for empty values and zero-byte types
• Add comprehensive regression test for ZST handling in shadow memory

Fixes: #8284

• 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.

[codecov]

Codecov Report

❌ Patch coverage is 85.71429% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 80.41%. Comparing base (59d2211) to head (0a3e8d5).

Files with missing lines	Patch %	Lines
src/goto-symex/shadow_memory_util.cpp	85.71%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8894      +/-   ##
===========================================
- Coverage    80.41%   80.41%   -0.01%     
===========================================
  Files         1703     1703              
  Lines       188398   188405       +7     
  Branches        73       73              
===========================================
- Hits        151502   151501       -1     
- Misses       36896    36904       +8     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[Copilot]

Pull request overview

Fixes a CBMC crash when aggregating shadow-memory values over zero-sized types (ZSTs), ensuring shadow-memory get operations return a well-defined default instead of creating invalid zero-width/empty-operand bitvector expressions.

Changes:

• Return a default zero value when aggregating over an empty set of values (e.g., structs whose non-padding components are all ZSTs).
• Skip zero-sized struct/union components during boolean aggregation to avoid generating invalid expressions.
• Add a regression test covering nested/only-ZST structs and shadow-memory get/set scenarios that previously triggered solver invariant violations.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/goto-symex/shadow_memory_util.cpp	Avoids constructing invalid aggregation expressions for ZST/empty-byte cases by skipping ZST components and returning a default zero value when there are no bytes/operands.
regression/cbmc-shadow-memory/zero-sized-types/test.desc	Adds a new regression test configuration (gcc-only) validating successful verification and guarding against warnings.
regression/cbmc-shadow-memory/zero-sized-types/main.c	Exercises shadow-memory operations over structs containing ZST fields (including nested and only-ZST cases) to prevent regressions of the crash.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.