split test suite generation out of cbmc/jbmc #2144
Conversation
kroening
requested review from
cesaro,
chrisr-diffblue,
mgudemann and
smowton
as code owners
src/Makefile
Outdated
| assembler analyses java_bytecode \ | ||
| DIRS = ansi-c big-int cbmc ccover jbmc cpp goto-cc goto-instrument \ | ||
| goto-programs goto-symex langapi pointer-analysis solvers util \ | ||
| linking xmllang assembler analyses java_bytecode \ |
There was a problem hiding this comment.
To avoid future changes of this kind (reformatting of several lines just because one word changed), could each entry please be put on a separate line like other Makefiles now do?
src/ccover/ccover_bmc.cpp
Outdated
| #include "ccover_bmc.h" | ||
|
|
||
| #include <chrono> | ||
| #include <iostream> |
There was a problem hiding this comment.
Is that actually required?
src/ccover/ccover_bmc.h
Outdated
| #include <util/invariant.h> | ||
| #include <util/options.h> | ||
| #include <util/ui_message.h> | ||
| #include <util/decision_procedure.h> |
src/ccover/ccover_bmc.h
Outdated
| #include <map> | ||
|
|
||
| #include <util/invariant.h> | ||
| #include <util/options.h> |
There was a problem hiding this comment.
A forward declaration of class optionst; would suffice. invariant.h seems unused here.
src/ccover/ccover_bmc.h
Outdated
| #include <goto-symex/symex_target_equation.h> | ||
| #include <goto-programs/goto_model.h> | ||
| #include <goto-programs/safety_checker.h> | ||
| #include <goto-symex/memory_model.h> |
There was a problem hiding this comment.
I'm not sure all of the above are needed.
src/ccover/ccover_parse_options.h
Outdated
|
|
||
| #include <util/ui_message.h> | ||
| #include <util/parse_options.h> | ||
| //#include <util/timestamper.h> |
src/ccover/ccover_parse_options.h
Outdated
|
|
||
| #include <langapi/language.h> | ||
|
|
||
| //#include <analyses/goto_check.h> |
| @@ -1,6 +1,5 @@ | |||
| SRC = all_properties.cpp \ | |||
| bmc.cpp \ | |||
| bmc_cover.cpp \ | |||
There was a problem hiding this comment.
This has already been moved in the previous commit, hence the prior commit yields an inconsistent state.
src/cbmc/cbmc_parse_options.cpp
Outdated
| // generate unwinding assumptions otherwise | ||
| options.set_option( | ||
| "partial-loops", | ||
| cmdline.isset("partial-loops")); |
There was a problem hiding this comment.
Seems unrelated and unnecessary?
src/jbmc/Makefile
Outdated
| @@ -30,6 +27,9 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ | |||
| ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ | |||
| ../goto-instrument/cover_instrument_other$(OBJEXT) \ | |||
| ../goto-instrument/cover_util$(OBJEXT) \ | |||
| ../goto-instrument/full_slicer$(OBJEXT) \ | |||
| ../goto-instrument/reachability_slicer$(OBJEXT) \ | |||
| ../goto-instrument/nondet_static$(OBJEXT) \ | |||
|
|
||
| #include <linking/static_lifetime_init.h> | ||
|
|
||
| void ccover_bmct::do_conversion() |
There was a problem hiding this comment.
Ideally, there should be a generic BMC class that provides these building block to avoid duplication.
There was a problem hiding this comment.
I don't see how this can be done in <2 years
| " cccover file.c ... source file names\n" | ||
| "\n" | ||
| "Test suite generation options:\n" | ||
| " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) |
There was a problem hiding this comment.
What is the default behaviour if this option is not given?
src/ccover/ccover_bmc.cpp
Outdated
| ::slice(equation); | ||
| statistics() << "slicing removed " | ||
| << equation.count_ignored_SSA_steps() | ||
| << " assignments"<<eom; |
| ui_message_handler.set_verbosity(v); | ||
| } | ||
|
|
||
| void ccover_parse_optionst::get_command_line_options(optionst &options) |
There was a problem hiding this comment.
Just as a note: Most of this code is duplicated in at least 8 different tools, which is not ideal. I'm not saying that needs to be fixed in this PR, but it has become difficult to distinguish intended from spurious differences between the command line interfaces.
|
I think this PR is right in setting a long-term direction, but as @peterschrammel also said: there should be de-duplication. In my opinion there should first be one or more PRs to implement de-duplication, and then this one should follow. |
kroening
force-pushed
the
ccover
branch
2 times, most recently
from
95b4929 to
bb93957
Compare
|
I note that all-properties (not-stop-on-fail) mode and cover mode have a lot in common, can they be factored? |
|
I factored out the unwindset parsing. |
kroening
force-pushed
the
ccover
branch
4 times, most recently
from
1e6f7a6 to
4b2a1a2
Compare
kroening
force-pushed
the
ccover
branch
4 times, most recently
from
5173042 to
1c950d9
Compare
kroening
force-pushed
the
ccover
branch
2 times, most recently
from
5119d43 to
3247fb9
Compare
|
I'm listed as a code owner but I think that's for about 4 lines of the change so I'm probably not the best person to review this. Splitting out coverage and BMC may be an idea but this PR seems to cover a bunch of other things as well. |
|
I am closing this PR as it seems to be very stale in terms of the current state of the branch it aims to merge to, and in terms of CI checks. If you would like to see this revived, please feel free to reopen the PR, and continue working on this after it has been rebased on top of |
No description provided.