Add remove_java_new pass to jdiff and janalyzer tools#8787
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Add remove_java_new pass to jdiff and janalyzer tools#8787tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8787 +/- ##
===========================================
+ Coverage 80.41% 80.43% +0.01%
===========================================
Files 1703 1703
Lines 188398 188406 +8
Branches 73 73
===========================================
+ Hits 151498 151537 +39
+ Misses 36900 36869 -31 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Add the `remove_java_new` pass after `convert_java_nondet` to both `jdiff` and `janalyzer`. This ensures that any new statements introduced by `convert_java_nondet` are properly processed. Fixes: diffblue#3094
tautschnig
force-pushed
the
fix-3094-remove_java_new
branch
from
0e55409 to
b951207
Compare
There was a problem hiding this comment.
Pull request overview
This PR updates the JBMC Java tooling pipelines so that Java nondet conversion is followed by remove_java_new, ensuring any new side effects introduced during nondet expansion are lowered before subsequent processing.
Changes:
- Add
convert_nondet+remove_java_newintojdiff’sprocess_goto_programpass sequence. - Add
convert_nondet+remove_java_newintojanalyzer’s per-functionprocess_goto_functionpass sequence.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
jbmc/src/jdiff/jdiff_parse_options.cpp |
Runs Java nondet conversion and then lowers any introduced java_new side effects in the whole-model processing pipeline. |
jbmc/src/janalyzer/janalyzer_parse_options.cpp |
Runs Java nondet conversion and then lowers java_new side effects in the per-function processing pipeline. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+701
to
+706
| // convert Java nondet expressions | ||
| java_object_factory_parameterst object_factory_parameters; | ||
| object_factory_parameters.set(options); | ||
| convert_nondet( | ||
| function, ui_message_handler, object_factory_parameters, ID_java); | ||
|
|
Comment on lines
+701
to
+712
| // convert Java nondet expressions | ||
| java_object_factory_parameterst object_factory_parameters; | ||
| object_factory_parameters.set(options); | ||
| convert_nondet( | ||
| function, ui_message_handler, object_factory_parameters, ID_java); | ||
|
|
||
| // remove Java new expressions (must be after convert_nondet) | ||
| remove_java_new( | ||
| function.get_function_id(), | ||
| function.get_goto_function(), | ||
| symbol_table, | ||
| ui_message_handler); |
Comment on lines
+204
to
+208
| // convert Java nondet expressions | ||
| java_object_factory_parameterst object_factory_parameters; | ||
| object_factory_parameters.set(options); | ||
| convert_nondet(goto_model, ui_message_handler, object_factory_parameters); | ||
|
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add the
remove_java_newpass afterconvert_java_nondetto bothjdiffandjanalyzer. This ensures that any new statements introduced byconvert_java_nondetare properly processed.Fixes: #3094