Skip to content

Commit f4eb1da

Browse files
author
Daniel Kroening
committed
cleanout test suite generation from cbmc
1 parent 4fe02e4 commit f4eb1da

File tree

9 files changed

+9
-52
lines changed

9 files changed

+9
-52
lines changed

‎jbmc/src/jbmc/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
4040
../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
4141
../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
4242
../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
43-
../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
4443
../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
4544
../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
4645
../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \

‎jbmc/src/jbmc/jbmc_parse_options.cpp

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

124-
if(cmdline.isset("cover"))
125-
parse_cover_options(cmdline, options);
126-
127124
if(cmdline.isset("nondet-static"))
128125
options.set_option("nondet-static", true);
129126

@@ -189,14 +186,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
189186
options.set_option("assumptions", false);
190187

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

201193
// generate unwinding assumptions otherwise
202194
options.set_option(
@@ -916,17 +908,9 @@ bool jbmc_parse_optionst::process_goto_functions(
916908
remove_unused_functions(goto_model, get_message_handler());
917909
}
918910

919-
// remove skips such that trivial GOTOs are deleted and not considered
920-
// for coverage annotation:
911+
// remove skips such that trivial GOTOs are deleted
921912
remove_skip(goto_model);
922913

923-
// instrument cover goals
924-
if(cmdline.isset("cover"))
925-
{
926-
if(instrument_cover_goals(options, goto_model, get_message_handler()))
927-
return true;
928-
}
929-
930914
// label the assertions
931915
// This must be done after adding assertions and
932916
// before using the argument of the "property" option.
@@ -970,7 +954,7 @@ bool jbmc_parse_optionst::process_goto_functions(
970954
full_slicer(goto_model);
971955
}
972956

973-
// remove any skips introduced since coverage instrumentation
957+
// remove any skips
974958
remove_skip(goto_model);
975959
}
976960

@@ -1079,7 +1063,6 @@ void jbmc_parse_optionst::help()
10791063
" --no-assertions ignore user assertions\n"
10801064
" --no-assumptions ignore user assumptions\n"
10811065
" --error-label label check that label is unreachable\n"
1082-
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
10831066
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
10841067
HELP_REACHABILITY_SLICER
10851068
" --full-slice run full slicer (experimental)\n" // NOLINT(*)

‎regression/cbmc-cover/Makefile

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -p -c ../../../src/ccover/ccover
55

66
tests.log: ../test.pl
7-
@../test.pl -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -p -c ../../../src/ccover/ccover
88

99
show:
1010
@for dir in *; do \

‎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

-6
Original file line numberDiff line numberDiff line change
@@ -380,12 +380,6 @@ safety_checkert::resultt bmct::execute(
380380
return safety_checkert::resultt::SAFE; // to indicate non-error
381381
}
382382

383-
if(!options.get_list_option("cover").empty())
384-
{
385-
return cover(goto_functions)?
386-
safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
387-
}
388-
389383
if(options.get_option("localize-faults")!="")
390384
{
391385
fault_localizationt fault_localization(

‎src/cbmc/bmc.h

-5
Original file line numberDiff line numberDiff line change
@@ -223,12 +223,7 @@ class bmct:public safety_checkert
223223
void slice();
224224
void show();
225225

226-
bool cover(const goto_functionst &goto_functions);
227-
228226
friend class bmc_all_propertiest;
229-
friend class bmc_covert;
230-
template <template <class goalt> class covert>
231-
friend class bmc_goal_covert;
232227
friend class fault_localizationt;
233228

234229
private:

‎src/cbmc/cbmc_parse_options.cpp

+1-13
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,6 @@ Author: Daniel Kroening, [email protected]
5757
#include <goto-instrument/reachability_slicer.h>
5858
#include <goto-instrument/full_slicer.h>
5959
#include <goto-instrument/nondet_static.h>
60-
#include <goto-instrument/cover.h>
6160

6261
#include <pointer-analysis/add_failed_symbols.h>
6362

@@ -151,9 +150,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
151150
if(cmdline.isset("show-vcc"))
152151
options.set_option("show-vcc", true);
153152

154-
if(cmdline.isset("cover"))
155-
parse_cover_options(cmdline, options);
156-
157153
if(cmdline.isset("mm"))
158154
options.set_option("mm", cmdline.get_value("mm"));
159155

@@ -786,13 +782,6 @@ bool cbmc_parse_optionst::process_goto_program(
786782
// for coverage annotation:
787783
remove_skip(goto_model);
788784

789-
// instrument cover goals
790-
if(options.is_set("cover"))
791-
{
792-
if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
793-
return true;
794-
}
795-
796785
// label the assertions
797786
// This must be done after adding assertions and
798787
// before using the argument of the "property" option.
@@ -831,7 +820,7 @@ bool cbmc_parse_optionst::process_goto_program(
831820
full_slicer(goto_model);
832821
}
833822

834-
// remove any skips introduced since coverage instrumentation
823+
// remove any skips
835824
remove_skip(goto_model);
836825
}
837826

@@ -937,7 +926,6 @@ void cbmc_parse_optionst::help()
937926
" --no-assertions ignore user assertions\n"
938927
" --no-assumptions ignore user assumptions\n"
939928
" --error-label label check that label is unreachable\n"
940-
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
941929
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
942930
HELP_REACHABILITY_SLICER
943931
" --full-slice run full slicer (experimental)\n" // NOLINT(*)

‎src/cbmc/cbmc_parse_options.h

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

‎unit/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,6 @@ testing-utils.dir:
6161
# We need to link bmc.o to the unit test, so here's everything it depends on...
6262
BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
6363
../src/cbmc/bmc$(OBJEXT) \
64-
../src/cbmc/bmc_cover$(OBJEXT) \
6564
../src/cbmc/bv_cbmc$(OBJEXT) \
6665
../src/cbmc/cbmc_dimacs$(OBJEXT) \
6766
../src/cbmc/cbmc_languages$(OBJEXT) \

0 commit comments

Comments
 (0)