Remove obsolete cbmc/fault_localization [blocks: 4216] #4215
Conversation
peterschrammel
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
kroening,
pkesseli,
smowton and
tautschnig
as code owners
peterschrammel
changed the title
src/cbmc/cbmc_parse_options.cpp
Outdated
| options, goto_model, ui_message_handler); | ||
| error() << "Given combination of command line arguments not supported" | ||
| << eom; | ||
| exit(CPROVER_EXIT_USAGE_ERROR); |
There was a problem hiding this comment.
Is this even possible? The branching structure above makes it a bit hard to see, actually. Could else if please be used above to reduce indent? If it is genuinely possible, the error message should say which command line options are at fault for that.
There was a problem hiding this comment.
Alternative in 1b72e9a.
There was a problem hiding this comment.
Can I ask for one level of indent by doing if(options.get_bool_option("localize-faults")) {...} else {...} to make the top level only decide on stop-on-fail+paths, in each of the (then) three cases?
There was a problem hiding this comment.
Nice! Which now makes clear that the final else is dead code, because you've enumerated all four combinations of paths/stop-on-fail.
| @@ -5,7 +5,6 @@ SRC = all_properties.cpp \ | |||
| cbmc_languages.cpp \ | |||
| cbmc_main.cpp \ | |||
| cbmc_parse_options.cpp \ | |||
| fault_localization.cpp \ | |||
There was a problem hiding this comment.
Can those Makefile changes please be in the same commit as the actual removal of the file?
tautschnig
changed the title
peterschrammel
force-pushed
the
remove-bmct-fault-localization
branch
from
fa25c94 to
126c0ab
Compare
reduces indentation
They are not used by any unit tests.
The goto-checker infrastructure is used now.
peterschrammel
force-pushed
the
remove-bmct-fault-localization
branch
from
126c0ab to
d9b910b
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 126c0ab).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102971681
Status will be re-evaluated on next push.
Common spurious failures:
-
the cbmc commit has disappeared in the mean time (e.g. in a force-push)
-
the author is not in the list of contributors (e.g. first-time contributors).
-
the compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: d9b910b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102973053
Status will be re-evaluated on next push.
Common spurious failures:
-
the cbmc commit has disappeared in the mean time (e.g. in a force-push)
-
the author is not in the list of contributors (e.g. first-time contributors).
-
the compatibility was already broken by an earlier merge.
Replaced by goto-checker infrastructure
Based on #3970 - last 3 commits