Skip to content

library_check: exclude tests.log from regression/cbmc-library scan - #9443

Open
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:pr/c-library-check-tests-log
Open

tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:pr/c-library-check-tests-log

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

library_check.sh enumerates regression/cbmc-library/ to build the list of expected test directories and cross-checks it against the library function table. The test runner (regression/test.pl) leaves a tests.log behind in that directory after a run, and on a subsequent cmake build the entry appears in __tests without a matching __functions line, aborting the build:

--- __tests
+++ __functions
-tests.log
Tests and library functions don't match.

This reliably breaks out-of-tree Docker builds after the host has run the regression suite once. Extend the egrep exclusion to skip tests.log alongside Makefile and CMakeLists.txt.

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

library_check.sh enumerates regression/cbmc-library/ to build the list
of expected test directories and cross-checks it against the library
function table.  The test runner (regression/test.pl) leaves a
tests.log behind in that directory after a run, and on a subsequent
cmake build the entry appears in __tests without a matching
__functions line, aborting the build:

  --- __tests
  +++ __functions
  -tests.log
  Tests and library functions don't match.

This reliably breaks out-of-tree Docker builds after the host has
run the regression suite once.  Extend the egrep exclusion to skip
tests.log alongside Makefile and CMakeLists.txt.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Copilot AI balanced review requested due to automatic review settings November 10, 2026 20:40

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota. Try requesting a review at a lower effort level.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.

@codecov

codecov Bot commented Nov 10, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 81.02%. Comparing base (826c1c7) to head (c90fe5f).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #9443   +/-   ##
========================================
  Coverage    81.02%   81.02%           
========================================
  Files         1723     1723           
  Lines       191314   191314           
  Branches        73       73           
========================================
  Hits        155020   155020           
  Misses       36294    36294           

☔ View full report in Codecov by Harness.
📢 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.

This branch has not been deployed

No deployments
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.

3 participants