Skip to content

Remove dubious module dependencies in goto-programs#8767

Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-571-unwanted-deps
Open

Remove dubious module dependencies in goto-programs#8767
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-571-unwanted-deps

Conversation

@tautschnig
Copy link
Collaborator

  • Move call_graph and does_remove_const from analyses to goto-programs
  • Move symex_target_equation graphml functions to goto-symex
  • Update module_dependencies.txt and build files accordingly
  • Refactor code to eliminate cross-module dependencies

Fixes: #571

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

@tautschnig tautschnig self-assigned this Feb 24, 2026
Move call_graph and does_remove_const from analyses to goto-programs
to eliminate the analyses dependency from goto-programs. Update build
files and include paths accordingly.

The goto-symex dependency in goto-programs (for GraphML witnesses) is
retained as it requires access to ansi-c and xmllang which are allowed
dependencies of goto-programs but not of goto-symex.

Fixes: diffblue#571

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig force-pushed the fix-571-unwanted-deps branch from 1a52fae to 62e1164 Compare March 19, 2026 09:07
@tautschnig tautschnig marked this pull request as ready for review March 19, 2026 09:10
@tautschnig tautschnig requested a review from a team as a code owner March 19, 2026 09:10
Copilot AI review requested due to automatic review settings March 19, 2026 09:10
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 restructures CBMC’s module layering to reduce “dubious” cross-module dependencies by relocating call-graph and const-removal utilities into goto-programs, and updating includes/build metadata accordingly (Fixes #571).

Changes:

  • Move call_graph / call_graph_helpers and does_remove_const usage over to goto-programs headers and sources.
  • Update unit tests and goto-instrument code to include the new goto-programs/* headers.
  • Adjust goto-programs build metadata to drop the analyses link dependency and update module dependency declarations.

Reviewed changes

Copilot reviewed 21 out of 21 changed files in this pull request and generated 1 comment.

Show a summary per file
File Description
unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp Switch unit test includes to goto-programs/does_remove_const.h.
unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp Switch unit test includes to goto-programs/does_remove_const.h.
unit/analyses/does_remove_const/does_remove_const_util.h Point test utility at goto-programs/does_remove_const.h.
unit/analyses/does_remove_const/does_expr_lose_const.cpp Switch unit test includes to goto-programs/does_remove_const.h.
unit/analyses/disconnect_unreachable_nodes_in_graph.cpp Update include to goto-programs/call_graph_helpers.h.
unit/analyses/call_graph.cpp Update includes to goto-programs/call_graph*.h.
src/goto-programs/slice_global_inits.cpp Replace analyses/call_graph.h include with local call_graph.h.
src/goto-programs/remove_function_pointers.cpp Replace analyses/does_remove_const.h include with local does_remove_const.h.
src/goto-programs/module_dependencies.txt Remove analyses dependency entry and update comments.
src/goto-programs/Makefile Add moved .cpp files to the goto-programs library build.
src/goto-programs/does_remove_const.h New home/header-guard for does_remove_const API.
src/goto-programs/does_remove_const.cpp New home for does_remove_const implementation.
src/goto-programs/CMakeLists.txt Drop analyses from goto-programs link dependencies.
src/goto-programs/call_graph.h New home/header-guard for call-graph API.
src/goto-programs/call_graph.cpp New home for call-graph implementation; include path updates/formatting.
src/goto-programs/call_graph_helpers.h New home/header-guard for call-graph helper API.
src/goto-programs/call_graph_helpers.cpp New home for call-graph helper implementation; formatting updates.
src/goto-instrument/goto_instrument_parse_options.cpp Update include to goto-programs/call_graph.h.
src/goto-instrument/aggressive_slicer.h Update include to goto-programs/call_graph.h.
src/goto-instrument/aggressive_slicer.cpp Update include to goto-programs/call_graph_helpers.h.
src/analyses/Makefile Remove moved sources from analyses library build list.
Comments suppressed due to low confidence (2)

src/goto-programs/call_graph.h:22

  • call_graph.h uses std::set, std::optional, std::unordered_map, and std::string in its public API (e.g., locationst, directed_grapht::get_node_index, nodes_by_name, format_callsites) but doesn't include the corresponding standard headers. This makes the header non-self-contained and can break builds depending on transitive includes. Add the missing includes (e.g., <set>, <optional>, <unordered_map>, <string>).
    src/goto-programs/does_remove_const.h:26
  • does_remove_const.h forward-declares source_locationt but exposes it by value inside std::pair<bool, source_locationt> in the operator()() signature. Because std::pair needs a complete source_locationt, this header isn't self-contained and can fail to compile in translation units that include it without also including util/source_location.h. Include <util/source_location.h> here (or change the API to avoid returning source_locationt by value).

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

@@ -1,8 +1,7 @@
analyses # dubious - concerns call_graph and does_remove_const
ansi-c # for GraphML witnesses
architecture # system
@codecov
Copy link

codecov bot commented Mar 19, 2026

Codecov Report

❌ Patch coverage is 84.61538% with 6 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.41%. Comparing base (4fe3ade) to head (62e1164).
⚠️ Report is 111 commits behind head on develop.

Files with missing lines Patch % Lines
src/goto-programs/call_graph.cpp 81.81% 6 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8767      +/-   ##
===========================================
+ Coverage    79.93%   80.41%   +0.47%     
===========================================
  Files         1698     1703       +5     
  Lines       187698   188397     +699     
  Branches        73       73              
===========================================
+ Hits        150034   151495    +1461     
+ Misses       37664    36902     -762     

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

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.

Cleanup unwanted dependencies between CBMC modules

2 participants