Skip to content

Commit 1e6f7a6

Browse files
author
Daniel Kroening
committed
cleanout test suite generation from cbmc
1 parent 8a62a2a commit 1e6f7a6

File tree

7 files changed

+10
-56
lines changed

7 files changed

+10
-56
lines changed

‎src/cbmc/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
SRC = all_properties.cpp \
22
bmc.cpp \
3-
bmc_cover.cpp \
43
bv_cbmc.cpp \
54
cbmc_dimacs.cpp \
65
cbmc_languages.cpp \

‎src/cbmc/bmc.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -382,14 +382,6 @@ safety_checkert::resultt bmct::execute(
382382
return safety_checkert::resultt::SAFE; // to indicate non-error
383383
}
384384

385-
if(!options.get_list_option("cover").empty())
386-
{
387-
const optionst::value_listt criteria=
388-
options.get_list_option("cover");
389-
return cover(goto_functions, criteria)?
390-
safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
391-
}
392-
393385
if(options.get_option("localize-faults")!="")
394386
{
395387
fault_localizationt fault_localization(

‎src/cbmc/bmc.h

-7
Original file line numberDiff line numberDiff line change
@@ -213,14 +213,7 @@ class bmct:public safety_checkert
213213
void slice();
214214
void show();
215215

216-
bool cover(
217-
const goto_functionst &goto_functions,
218-
const optionst::value_listt &criteria);
219-
220216
friend class bmc_all_propertiest;
221-
friend class bmc_covert;
222-
template <template <class goalt> class covert>
223-
friend class bmc_goal_covert;
224217
friend class fault_localizationt;
225218

226219
private:

‎src/cbmc/cbmc_parse_options.cpp

+1-13
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,6 @@ Author: Daniel Kroening, [email protected]
5555
#include <goto-instrument/reachability_slicer.h>
5656
#include <goto-instrument/full_slicer.h>
5757
#include <goto-instrument/nondet_static.h>
58-
#include <goto-instrument/cover.h>
5958

6059
#include <pointer-analysis/add_failed_symbols.h>
6160

@@ -162,9 +161,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
162161
if(cmdline.isset("show-vcc"))
163162
options.set_option("show-vcc", true);
164163

165-
if(cmdline.isset("cover"))
166-
parse_cover_options(cmdline, options);
167-
168164
if(cmdline.isset("mm"))
169165
options.set_option("mm", cmdline.get_value("mm"));
170166

@@ -789,13 +785,6 @@ bool cbmc_parse_optionst::process_goto_program(
789785
// for coverage annotation:
790786
remove_skip(goto_model);
791787

792-
// instrument cover goals
793-
if(options.is_set("cover"))
794-
{
795-
if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
796-
return true;
797-
}
798-
799788
// label the assertions
800789
// This must be done after adding assertions and
801790
// before using the argument of the "property" option.
@@ -834,7 +823,7 @@ bool cbmc_parse_optionst::process_goto_program(
834823
full_slicer(goto_model);
835824
}
836825

837-
// remove any skips introduced since coverage instrumentation
826+
// remove any skips
838827
remove_skip(goto_model);
839828
}
840829

@@ -947,7 +936,6 @@ void cbmc_parse_optionst::help()
947936
" --no-assertions ignore user assertions\n"
948937
" --no-assumptions ignore user assumptions\n"
949938
" --error-label label check that label is unreachable\n"
950-
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
951939
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
952940
HELP_REACHABILITY_SLICER
953941
" --full-slice run full slicer (experimental)\n" // NOLINT(*)

‎src/cbmc/cbmc_parse_options.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ class optionst;
6363
"(error-label):(verbosity):(no-library)" \
6464
"(nondet-static)" \
6565
"(version)" \
66-
"(cover):(symex-coverage-report):" \
66+
"(symex-coverage-report):" \
6767
"(mm):" \
6868
OPT_TIMESTAMP \
6969
"(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \

‎src/jbmc/Makefile

+3-4
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1717
../pointer-analysis/add_failed_symbols$(OBJEXT) \
1818
../pointer-analysis/rewrite_index$(OBJEXT) \
1919
../pointer-analysis/goto_program_dereference$(OBJEXT) \
20-
../goto-instrument/full_slicer$(OBJEXT) \
21-
../goto-instrument/reachability_slicer$(OBJEXT) \
22-
../goto-instrument/nondet_static$(OBJEXT) \
2320
../goto-instrument/cover$(OBJEXT) \
2421
../goto-instrument/cover_basic_blocks$(OBJEXT) \
2522
../goto-instrument/cover_filter$(OBJEXT) \
@@ -30,6 +27,9 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
3027
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
3128
../goto-instrument/cover_instrument_other$(OBJEXT) \
3229
../goto-instrument/cover_util$(OBJEXT) \
30+
../goto-instrument/full_slicer$(OBJEXT) \
31+
../goto-instrument/reachability_slicer$(OBJEXT) \
32+
../goto-instrument/nondet_static$(OBJEXT) \
3333
../analyses/analyses$(LIBEXT) \
3434
../langapi/langapi$(LIBEXT) \
3535
../xmllang/xmllang$(LIBEXT) \
@@ -40,7 +40,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
4040
../json/json$(LIBEXT) \
4141
../cbmc/all_properties$(OBJEXT) \
4242
../cbmc/bmc$(OBJEXT) \
43-
../cbmc/bmc_cover$(OBJEXT) \
4443
../cbmc/bv_cbmc$(OBJEXT) \
4544
../cbmc/cbmc_dimacs$(OBJEXT) \
4645
../cbmc/cbmc_solvers$(OBJEXT) \

‎src/jbmc/jbmc_parse_options.cpp

+5-22
Original file line numberDiff line numberDiff line change
@@ -117,9 +117,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
117117
if(cmdline.isset("show-vcc"))
118118
options.set_option("show-vcc", true);
119119

120-
if(cmdline.isset("cover"))
121-
parse_cover_options(cmdline, options);
122-
123120
if(cmdline.isset("no-simplify"))
124121
options.set_option("simplify", false);
125122
else
@@ -190,14 +187,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
190187
options.set_option("error-label", cmdline.get_values("error-label"));
191188

192189
// generate unwinding assertions
193-
if(cmdline.isset("cover"))
194-
options.set_option("unwinding-assertions", false);
195-
else
196-
{
197-
options.set_option(
198-
"unwinding-assertions",
199-
cmdline.isset("unwinding-assertions"));
200-
}
190+
options.set_option(
191+
"unwinding-assertions",
192+
cmdline.isset("unwinding-assertions"));
201193

202194
// generate unwinding assumptions otherwise
203195
options.set_option(
@@ -927,17 +919,9 @@ bool jbmc_parse_optionst::process_goto_functions(
927919
remove_unused_functions(goto_model, get_message_handler());
928920
}
929921

930-
// remove skips such that trivial GOTOs are deleted and not considered
931-
// for coverage annotation:
922+
// remove skips such that trivial GOTOs are deleted
932923
remove_skip(goto_model);
933924

934-
// instrument cover goals
935-
if(cmdline.isset("cover"))
936-
{
937-
if(instrument_cover_goals(options, goto_model, get_message_handler()))
938-
return true;
939-
}
940-
941925
// label the assertions
942926
// This must be done after adding assertions and
943927
// before using the argument of the "property" option.
@@ -981,7 +965,7 @@ bool jbmc_parse_optionst::process_goto_functions(
981965
full_slicer(goto_model);
982966
}
983967

984-
// remove any skips introduced since coverage instrumentation
968+
// remove any skips
985969
remove_skip(goto_model);
986970
goto_model.goto_functions.update();
987971
}
@@ -1053,7 +1037,6 @@ void jbmc_parse_optionst::help()
10531037
" --no-assertions ignore user assertions\n"
10541038
" --no-assumptions ignore user assumptions\n"
10551039
" --error-label label check that label is unreachable\n"
1056-
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
10571040
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
10581041
HELP_REACHABILITY_SLICER
10591042
" --full-slice run full slicer (experimental)\n" // NOLINT(*)

0 commit comments

Comments
 (0)