Remove undefined-function-is-assume-false from goto-instrument#8783
Remove undefined-function-is-assume-false from goto-instrument#8783tautschnig 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 #8783 +/- ##
========================================
Coverage 80.02% 80.02%
========================================
Files 1700 1700
Lines 188345 188323 -22
Branches 73 73
========================================
- Hits 150716 150704 -12
+ Misses 37629 37619 -10 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Users can like-for-like replace such use with `--generate-function-body '.*' --generate-function-body-options assume-false`. Fixes: diffblue#2070
1f663d2 to
fd0dc19
Compare
There was a problem hiding this comment.
Pull request overview
Removes the --undefined-function-is-assume-false command-line option and its implementation from goto-instrument, directing users to replace it with --generate-function-body '.*' --generate-function-body-options assume-false.
Changes:
- Deleted
undefined_function_abort_pathAPI and implementation. - Removed CLI option parsing and help/manpage documentation for
--undefined-function-is-assume-false. - Updated
goto-instrumentoption list to no longer advertise the removed flag.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| src/goto-instrument/undefined_functions.h | Removes the declaration for the deleted undefined-function instrumentation helper. |
| src/goto-instrument/undefined_functions.cpp | Removes the implementation that rewrote undefined calls to assume(false). |
| src/goto-instrument/goto_instrument_parse_options.h | Drops the CLI option from the recognized options list. |
| src/goto-instrument/goto_instrument_parse_options.cpp | Removes runtime handling and --help text for the option. |
| doc/man/goto-instrument.1 | Removes the manpage entry for the deleted option. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| "(" FLAG_ENFORCE_CONTRACT "):" \ | ||
| OPT_ENFORCE_CONTRACT_REC \ | ||
| "(show-threaded)(list-calls-args)" \ | ||
| "(undefined-function-is-assume-false)" \ | ||
| "(remove-function-body):" \ | ||
| "(remove-function-body-regex):" \ | ||
| OPT_AGGRESSIVE_SLICER \ |
There was a problem hiding this comment.
Removing --undefined-function-is-assume-false from the accepted option set is a breaking CLI change that will likely surface as a generic 'unknown option' error with no migration guidance. Consider keeping the option as a hidden/compatibility alias (not listed in --help/manpage), emitting a clear deprecation/removal diagnostic that points users to --generate-function-body '.*' --generate-function-body-options assume-false, and then exiting with a non-zero status (or optionally auto-translating it).
| " {y--undefined-function-is-assume-false} \t convert each call to an" | ||
| " undefined function to assume(false)\n" | ||
| HELP_INSERT_FINAL_ASSERT_FALSE | ||
| HELP_REPLACE_FUNCTION_BODY |
There was a problem hiding this comment.
The PR description introduces a specific like-for-like replacement for --undefined-function-is-assume-false, but after removing the help entry there is no remaining discoverable hint in --help. Consider adding a short migration note near the relevant HELP_REPLACE_FUNCTION_BODY/function-body generation help text so users can find the recommended replacement without consulting the PR/issue.
| HELP_REPLACE_FUNCTION_BODY | |
| HELP_REPLACE_FUNCTION_BODY | |
| " Note: the option --undefined-function-is-assume-false has been removed; an" | |
| " equivalent effect can be achieved using --replace-function-body with a body" | |
| " that calls __CPROVER_assume(false).\n" |
Users can like-for-like replace such use with
--generate-function-body '.*' --generate-function-body-options assume-false.Fixes: #2070