Skip to content

Initialise message_handler in bv_refinement unit test#8863

Merged
kroening merged 2 commits intodiffblue:developfrom
tautschnig:asan-fixes/bv_refinement
Mar 16, 2026
Merged

Initialise message_handler in bv_refinement unit test#8863
kroening merged 2 commits intodiffblue:developfrom
tautschnig:asan-fixes/bv_refinement

Conversation

@tautschnig
Copy link
Collaborator

The message_handler member of bv_refinementt::infot was left uninitialised, which is undefined behaviour when it is later dereferenced. Set it to null_message_handler.

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

@tautschnig tautschnig self-assigned this Mar 15, 2026
Copilot AI review requested due to automatic review settings March 15, 2026 21:24
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR fixes undefined behavior in a JBMC unit test by ensuring bv_refinementt::infot::message_handler is initialized before being dereferenced.

Changes:

  • Initialize bv_refinementt::infot::message_handler to null_message_handler in the instantiate_not_contains unit test helper.

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

@codecov
Copy link

codecov bot commented Mar 15, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.41%. Comparing base (eee45a7) to head (ec7cebe).
⚠️ Report is 7 commits behind head on develop.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8863      +/-   ##
===========================================
+ Coverage    80.00%   80.41%   +0.40%     
===========================================
  Files         1703     1703              
  Lines       188397   188398       +1     
  Branches        73       73              
===========================================
+ Hits        150736   151496     +760     
+ Misses       37661    36902     -759     

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

tautschnig and others added 2 commits March 16, 2026 10:44
The message_handler member of bv_refinementt::infot was left
uninitialised, which is undefined behaviour when it is later
dereferenced. Set it to null_message_handler.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
These tests were missing the CORE label, so they were excluded from
coverage collection (ctest -V -L CORE). This meant XFAIL test code
never executed during coverage runs, producing 0% coverage for any
changes to XFAIL tests.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig force-pushed the asan-fixes/bv_refinement branch from 942d70e to ec7cebe Compare March 16, 2026 10:44
@kroening kroening merged commit 85c204f into diffblue:develop Mar 16, 2026
41 of 43 checks passed
@tautschnig tautschnig deleted the asan-fixes/bv_refinement branch March 16, 2026 20:18
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.

4 participants