Convert unit tests to Catch framework and fix compilation issues by tautschnig · Pull Request #8760 · diffblue/cbmc

tautschnig · 2025-11-30T03:15:14Z

We had some pre-Catch-era unit tests still lying around unmaintained and unused. Alas, they wouldn't even compile anymore. Compilation issues are now fixed and they are embedded in the Catch framework.

Fixes: #879

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

Move unit/cpp_parser.cpp to unit/cpp/cpp_parser.cpp, convert from standalone main() to Catch TEST_CASE, and add module_dependencies.txt. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Move unit/cpp_scanner.cpp to unit/cpp/cpp_scanner.cpp, convert from standalone main() to Catch TEST_CASE, and fix scanner initialization to use the token buffer's internal ansi_c_parser. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Move unit/elf_reader.cpp to unit/goto-programs/elf_reader.cpp, convert from standalone main() to Catch TEST_CASE, and update exception type from const char* to deserialization_exceptiont. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

codecov · 2026-03-06T22:34:06Z

Codecov Report

❌ Patch coverage is 97.94721% with 7 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.05%. Comparing base (eaaf029) to head (9b88166).

Files with missing lines	Patch %	Lines
unit/util/ieee_float.cpp	96.55%	5 Missing ⚠️
unit/goto-programs/wp.cpp	97.22%	2 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8760      +/-   ##
===========================================
+ Coverage    80.01%   80.05%   +0.03%     
===========================================
  Files         1700     1707       +7     
  Lines       188338   188791     +453     
  Branches        73       73              
===========================================
+ Hits        150695   151129     +434     
- Misses       37643    37662      +19

☔ 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

This PR modernizes a set of legacy unit tests by converting them to the Catch framework, fixing prior compilation issues, and ensuring they are built as part of the unit test suite (Fixes #879).

Changes:

Replaced old standalone main()-based test programs with Catch TEST_CASEs for JSON parsing, SMT2 parsing, ELF reading, weakest precondition, and C++ parser/scanner.
Updated unit test build integration (CMake and Makefile) and module dependency declarations to include the new tests.
Removed the previously excluded/non-building legacy unit test sources.

Reviewed changes

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

Show a summary per file

File	Description
unit/wp.cpp	Removes legacy standalone WP test program.
unit/util/module_dependencies.txt	Adds `json` dependency for util unit tests.
unit/util/json.cpp	Adds Catch-based JSON parser unit tests.
unit/util/ieee_float.cpp	Extends IEEE-float unit tests; adds randomized arithmetic/comparison/conversion coverage.
unit/solvers/smt2/smt2_parser.cpp	Adds Catch-based SMT2 parser unit tests.
unit/smt2_parser.cpp	Removes legacy standalone SMT2 parser test program.
unit/json.cpp	Removes legacy standalone JSON parser test program.
unit/ieee_float.cpp	Removes legacy standalone IEEE float test program.
unit/goto-programs/wp.cpp	Adds Catch-based weakest-precondition unit tests using a temporary C file.
unit/goto-programs/module_dependencies.txt	Adds `langapi` dependency for goto-programs unit tests.
unit/goto-programs/elf_reader.cpp	Adds Catch-based ELF reader unit tests.
unit/elf_reader.cpp	Removes legacy standalone ELF reader test program.
unit/cpp_scanner.cpp	Removes legacy standalone C++ scanner test program.
unit/cpp_parser.cpp	Removes legacy standalone C++ parser test program.
unit/cpp/module_dependencies.txt	Declares dependencies for new `unit/cpp/*` tests.
unit/cpp/cpp_scanner.cpp	Adds Catch-based C++ scanner/tokenization unit tests.
unit/cpp/cpp_parser.cpp	Adds Catch-based C++ parser unit tests.
unit/Makefile	Adds new unit test sources to the Makefile build.
unit/CMakeLists.txt	Stops excluding the old non-building test sources so new Catch tests are included via glob.

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

unit/util/ieee_float.cpp

unit/goto-programs/wp.cpp

Move unit/wp.cpp to unit/goto-programs/wp.cpp, convert from standalone main() to Catch TEST_CASE, and fix API changes: ansi_c_languaget no longer takes message_handler in constructor, parse()/typecheck() now require message_handlert&, and goto_instructiont members code/guard are now accessed via code()/condition() methods. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Move unit/json.cpp to unit/util/json.cpp and convert from standalone main() to Catch TEST_CASE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Move unit/smt2_parser.cpp to unit/solvers/smt2/smt2_parser.cpp and rewrite completely. The old test subclassed smt2_parsert with virtual callback overrides, but the parser API has been redesigned and no longer supports that pattern. The new test uses the current API directly (parse(), exit flag, id_map). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Move unit/ieee_float.cpp to unit/util/ieee_float.cpp (merging into the existing file), convert from standalone main() to Catch TEST_CASE, and fix API changes: use ieee_floatt with rounding mode for arithmetic operators, change ieee_equal/ieee_not_equal from free functions to member calls, use ieee_floatt for build(), and add #include <cfloat>. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The old unit/osx_fat_reader.cpp was removed in ad5c4f9. The exclusion line in CMakeLists.txt is now dead code. A proper Catch test already exists at unit/goto-programs/osx_fat_reader.cpp. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig self-assigned this Feb 24, 2026

tautschnig and others added 3 commits March 6, 2026 20:06

Convert cpp_parser unit test to Catch framework

43a8e4d

Move unit/cpp_parser.cpp to unit/cpp/cpp_parser.cpp, convert from standalone main() to Catch TEST_CASE, and add module_dependencies.txt. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the fix-879-convert-unit-tests branch 2 times, most recently from 1e96a2b to f8710c1 Compare March 6, 2026 21:44

tautschnig marked this pull request as ready for review March 7, 2026 20:39

Copilot AI review requested due to automatic review settings March 7, 2026 20:39

Copilot started reviewing on behalf of tautschnig March 7, 2026 20:40 View session

Copilot AI reviewed Mar 7, 2026

View reviewed changes

tautschnig and others added 5 commits March 8, 2026 22:53

Convert json unit test to Catch framework

1f8541c

Move unit/json.cpp to unit/util/json.cpp and convert from standalone main() to Catch TEST_CASE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the fix-879-convert-unit-tests branch from f8710c1 to 9b88166 Compare March 8, 2026 22:54

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Mar 9, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Convert unit tests to Catch framework and fix compilation issues#8760

Convert unit tests to Catch framework and fix compilation issues#8760
tautschnig wants to merge 8 commits intodiffblue:developfrom
tautschnig:fix-879-convert-unit-tests

tautschnig commented Nov 30, 2025

Uh oh!

codecov bot commented Mar 6, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

tautschnig commented Nov 30, 2025

Uh oh!

codecov bot commented Mar 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

codecov bot commented Mar 6, 2026 •

edited

Loading