Skip to content

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Sep 16, 2025

Note to reviewers: please review commit-by-commit.

Adds a parser for JSON-encoded goto_functionst and support to symtab2gb to optionally read such from a file and store them in goto_functions of a goto_modelt.

  • 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.
  • 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 Sep 16, 2025
@tautschnig tautschnig force-pushed the goto-functions-json branch 4 times, most recently from e39b7d5 to f4fd908 Compare September 17, 2025 09:35
Use an approach similar to contracts regression tests to extract
parameters for multiple tools from a single line in the .desc file. This
avoids overly fragmenting regression tests.
The C front-end created symbols that had the function set to an empty
string. This was not accurately represented in the JSON representation,
but also shouldn't be used at all. Thus, changing the parser rather than
the JSON serialisation.
We were previously only printing a subset, making it impossible to
restore a `source_locationt` from its JSON representation.
The JSON output of a `source_locationt` is different from generic
`irept`.

Also, make `try_get_{bool,string}` publicly available for subsequent
re-use.
We must include all information required to re-produce a goto program
from its JSON representation.
Copy link

codecov bot commented Sep 18, 2025

Codecov Report

❌ Patch coverage is 88.00461% with 104 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.43%. Comparing base (b0156a3) to head (6d3ce5d).
⚠️ Report is 7 commits behind head on develop.

Files with missing lines Patch % Lines
src/json-symtab-language/json_goto_function.cpp 71.97% 51 Missing ⚠️
src/json-symtab-language/json_symbol.cpp 45.16% 34 Missing ⚠️
src/symtab2gb/symtab2gb_parse_options.cpp 31.81% 15 Missing ⚠️
src/json-symtab-language/json_goto_functions.cpp 92.85% 2 Missing ⚠️
src/util/json_irep.cpp 91.30% 2 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8713      +/-   ##
===========================================
+ Coverage    80.39%   80.43%   +0.03%     
===========================================
  Files         1688     1695       +7     
  Lines       207435   208285     +850     
  Branches        73       73              
===========================================
+ Hits        166776   167524     +748     
- Misses       40659    40761     +102     

☔ 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 goto-functions-json branch 3 times, most recently from 32637a1 to 1a105d5 Compare September 19, 2025 11:18
Adds a parser for JSON-encoded `goto_functionst` and support to
`symtab2gb` to optionally read such from a file and store them in
`goto_functions` of a `goto_modelt`.
@tautschnig tautschnig merged commit 5f4c82d into diffblue:develop Sep 19, 2025
41 checks passed
@tautschnig tautschnig deleted the goto-functions-json branch September 19, 2025 20:33
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