Skip to content

Set 20-minute timeout for all CMake-based regression tests#8848

Merged
tautschnig merged 3 commits intodiffblue:developfrom
tautschnig:test-timeout
Mar 9, 2026
Merged

Set 20-minute timeout for all CMake-based regression tests#8848
tautschnig merged 3 commits intodiffblue:developfrom
tautschnig:test-timeout

Conversation

@tautschnig
Copy link
Copy Markdown
Collaborator

Add TIMEOUT 1200 to the set_tests_properties call in both copies of the add_test_pl_profile macro (regression/CMakeLists.txt and regression/libcprover-cpp/CMakeLists.txt). This ensures CTest will kill and report as failed any regression test that exceeds 20 minutes, preventing CI jobs from hanging indefinitely on tests that time out.

  • 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 4, 2026
Copilot AI review requested due to automatic review settings March 4, 2026 14:52
Copy link
Copy Markdown

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

Adds a per-test timeout to the regression test infrastructure to prevent CI hangs from long-running tests.

Changes:

  • Enforce a 20-minute CTest timeout for CMake-registered regression tests.
  • Add an optional -t / TESTPL_TIMEOUT timeout to regression/test.pl, implemented via fork + alarm + process-group kill.
  • Update the test runner call chain to pass the timeout through to execution.

Reviewed changes

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

File Description
regression/test.pl Adds a per-test timeout option and enforces it by killing the test process group on timeout.
regression/CMakeLists.txt Adds TIMEOUT 1200 to CTest properties for regression tests.
regression/libcprover-cpp/CMakeLists.txt Adds TIMEOUT 1200 to CTest properties for regression tests in libcprover-cpp.

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

Comment thread regression/test.pl Outdated
Comment thread regression/test.pl
Comment thread regression/test.pl Outdated
@tautschnig tautschnig force-pushed the test-timeout branch 2 times, most recently from 560c68e to be53558 Compare March 4, 2026 15:55
@codecov
Copy link
Copy Markdown

codecov Bot commented Mar 4, 2026

Codecov Report

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

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8848   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1700     1700           
  Lines       188338   188338           
  Branches        73       73           
========================================
+ Hits        150695   150699    +4     
+ Misses       37643    37639    -4     

☔ 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 tautschnig force-pushed the test-timeout branch 4 times, most recently from 7291566 to 0614468 Compare March 5, 2026 20:54
tautschnig and others added 2 commits March 6, 2026 11:34
Add TIMEOUT 1200 to the set_tests_properties call in both copies of the
add_test_pl_profile macro (regression/CMakeLists.txt and
regression/libcprover-cpp/CMakeLists.txt). This ensures CTest will kill
and report as failed any regression test that exceeds 20 minutes,
preventing CI jobs from hanging indefinitely on tests that time out.

Co-authored-by: Kiro (autonomous agent) <kiro-agent@users.noreply.github.com>
Fork the test command into a new process group and use alarm() to enforce
an optional per-test timeout. When the timeout fires, kill the entire
process group with SIGKILL and report the test as failed with a TIMEOUT
marker.

The timeout can be set via -t <secs> on the command line or via the
TESTPL_TIMEOUT environment variable (command line takes precedence).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig force-pushed the test-timeout branch 2 times, most recently from 2c14354 to cbf0862 Compare March 8, 2026 20:14
Several JBMC and CBMC test suites exceed the 1200-second default timeout
on macOS-14 ARM CI runners, which can be 1.5x slower than typical runs.
Set per-suite timeouts based on ~2x the observed time on develop:

  contracts-dfcc-CORE                                  1800s (  827s on develop)
  strings-smoke-tests-symex-driven-lazy-loading-CORE   1800s (  766s on develop)
  jbmc-strings-CORE                                    1800s (  937s on develop)
  book-examples-cprover-smt2-CORE                      2400s ( 1074s on develop)
  jbmc-symex-driven-lazy-loading-CORE                  4800s ( 2385s on develop)
  jbmc-strings-symex-driven-lazy-loading-CORE         10800s ( 5583s on develop)

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig merged commit 9f78268 into diffblue:develop Mar 9, 2026
41 checks passed
@tautschnig tautschnig deleted the test-timeout branch March 9, 2026 15:47
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