Skip to content

Commit 21476dd

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #4583 from peterschrammel/remove-unnecessary-blocks
Remove unnecessary blocks
2 parents e1fe746 + 5bbd944 commit 21476dd

File tree

1 file changed

+163
-173
lines changed

1 file changed

+163
-173
lines changed

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 163 additions & 173 deletions
Original file line numberDiff line numberDiff line change
@@ -700,221 +700,211 @@ int cbmc_parse_optionst::get_goto_program(
700700
return CPROVER_EXIT_INCORRECT_TASK;
701701
}
702702

703-
{
704-
goto_model =
705-
initialize_goto_model(cmdline.args, ui_message_handler, options);
706-
707-
if(cmdline.isset("show-symbol-table"))
708-
{
709-
show_symbol_table(goto_model, ui_message_handler);
710-
return CPROVER_EXIT_SUCCESS;
711-
}
703+
goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
712704

713-
if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
714-
return CPROVER_EXIT_INTERNAL_ERROR;
705+
if(cmdline.isset("show-symbol-table"))
706+
{
707+
show_symbol_table(goto_model, ui_message_handler);
708+
return CPROVER_EXIT_SUCCESS;
709+
}
715710

716-
if(cmdline.isset("validate-goto-model"))
717-
{
718-
goto_model.validate();
719-
}
711+
if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
712+
return CPROVER_EXIT_INTERNAL_ERROR;
720713

721-
// show it?
722-
if(cmdline.isset("show-loops"))
723-
{
724-
show_loop_ids(ui_message_handler.get_ui(), goto_model);
725-
return CPROVER_EXIT_SUCCESS;
726-
}
714+
if(cmdline.isset("validate-goto-model"))
715+
{
716+
goto_model.validate();
717+
}
727718

728-
// show it?
729-
if(
730-
cmdline.isset("show-goto-functions") ||
731-
cmdline.isset("list-goto-functions"))
732-
{
733-
show_goto_functions(
734-
goto_model,
735-
ui_message_handler,
736-
cmdline.isset("list-goto-functions"));
737-
return CPROVER_EXIT_SUCCESS;
738-
}
719+
// show it?
720+
if(cmdline.isset("show-loops"))
721+
{
722+
show_loop_ids(ui_message_handler.get_ui(), goto_model);
723+
return CPROVER_EXIT_SUCCESS;
724+
}
739725

740-
log.status() << config.object_bits_info() << messaget::eom;
726+
// show it?
727+
if(
728+
cmdline.isset("show-goto-functions") ||
729+
cmdline.isset("list-goto-functions"))
730+
{
731+
show_goto_functions(
732+
goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
733+
return CPROVER_EXIT_SUCCESS;
741734
}
742735

736+
log.status() << config.object_bits_info() << messaget::eom;
737+
743738
return -1; // no error, continue
744739
}
745740

746741
void cbmc_parse_optionst::preprocessing(const optionst &options)
747742
{
743+
if(cmdline.args.size() != 1)
748744
{
749-
if(cmdline.args.size()!=1)
750-
{
751-
log.error() << "Please provide one program to preprocess"
752-
<< messaget::eom;
753-
return;
754-
}
745+
log.error() << "Please provide one program to preprocess" << messaget::eom;
746+
return;
747+
}
755748

756-
std::string filename=cmdline.args[0];
749+
std::string filename = cmdline.args[0];
757750

758-
std::ifstream infile(filename);
751+
std::ifstream infile(filename);
759752

760-
if(!infile)
761-
{
762-
log.error() << "failed to open input file" << messaget::eom;
763-
return;
764-
}
753+
if(!infile)
754+
{
755+
log.error() << "failed to open input file" << messaget::eom;
756+
return;
757+
}
765758

766-
std::unique_ptr<languaget> language=get_language_from_filename(filename);
767-
language->set_language_options(options);
759+
std::unique_ptr<languaget> language = get_language_from_filename(filename);
760+
language->set_language_options(options);
768761

769-
if(language==nullptr)
770-
{
771-
log.error() << "failed to figure out type of file" << messaget::eom;
772-
return;
773-
}
762+
if(language == nullptr)
763+
{
764+
log.error() << "failed to figure out type of file" << messaget::eom;
765+
return;
766+
}
774767

775-
language->set_message_handler(ui_message_handler);
768+
language->set_message_handler(ui_message_handler);
776769

777-
if(language->preprocess(infile, filename, std::cout))
778-
log.error() << "PREPROCESSING ERROR" << messaget::eom;
779-
}
770+
if(language->preprocess(infile, filename, std::cout))
771+
log.error() << "PREPROCESSING ERROR" << messaget::eom;
780772
}
781773

782774
bool cbmc_parse_optionst::process_goto_program(
783775
goto_modelt &goto_model,
784776
const optionst &options,
785777
messaget &log)
786778
{
779+
// Remove inline assembler; this needs to happen before
780+
// adding the library.
781+
remove_asm(goto_model);
782+
783+
// add the library
784+
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
785+
<< messaget::eom;
786+
link_to_library(
787+
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
788+
link_to_library(
789+
goto_model, log.get_message_handler(), cprover_c_library_factory);
790+
791+
if(options.get_bool_option("string-abstraction"))
792+
string_instrumentation(goto_model, log.get_message_handler());
793+
794+
// remove function pointers
795+
log.status() << "Removal of function pointers and virtual functions"
796+
<< messaget::eom;
797+
remove_function_pointers(
798+
log.get_message_handler(),
799+
goto_model,
800+
options.get_bool_option("pointer-check"));
801+
802+
mm_io(goto_model);
803+
804+
// instrument library preconditions
805+
instrument_preconditions(goto_model);
806+
807+
// remove returns, gcc vectors, complex
808+
remove_returns(goto_model);
809+
remove_vector(goto_model);
810+
remove_complex(goto_model);
811+
rewrite_union(goto_model);
812+
813+
// add generic checks
814+
log.status() << "Generic Property Instrumentation" << messaget::eom;
815+
goto_check(options, goto_model);
816+
817+
// checks don't know about adjusted float expressions
818+
adjust_float_expressions(goto_model);
819+
820+
// ignore default/user-specified initialization
821+
// of variables with static lifetime
822+
if(options.get_bool_option("nondet-static"))
787823
{
788-
// Remove inline assembler; this needs to happen before
789-
// adding the library.
790-
remove_asm(goto_model);
791-
792-
// add the library
793-
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
794-
<< messaget::eom;
795-
link_to_library(
796-
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
797-
link_to_library(
798-
goto_model, log.get_message_handler(), cprover_c_library_factory);
799-
800-
if(options.get_bool_option("string-abstraction"))
801-
string_instrumentation(goto_model, log.get_message_handler());
802-
803-
// remove function pointers
804-
log.status() << "Removal of function pointers and virtual functions"
824+
log.status() << "Adding nondeterministic initialization "
825+
"of static/global variables"
805826
<< messaget::eom;
806-
remove_function_pointers(
807-
log.get_message_handler(),
808-
goto_model,
809-
options.get_bool_option("pointer-check"));
810-
811-
mm_io(goto_model);
812-
813-
// instrument library preconditions
814-
instrument_preconditions(goto_model);
815-
816-
// remove returns, gcc vectors, complex
817-
remove_returns(goto_model);
818-
remove_vector(goto_model);
819-
remove_complex(goto_model);
820-
rewrite_union(goto_model);
821-
822-
// add generic checks
823-
log.status() << "Generic Property Instrumentation" << messaget::eom;
824-
goto_check(options, goto_model);
825-
826-
// checks don't know about adjusted float expressions
827-
adjust_float_expressions(goto_model);
828-
829-
// ignore default/user-specified initialization
830-
// of variables with static lifetime
831-
if(options.get_bool_option("nondet-static"))
832-
{
833-
log.status() << "Adding nondeterministic initialization "
834-
"of static/global variables"
835-
<< messaget::eom;
836-
nondet_static(goto_model);
837-
}
827+
nondet_static(goto_model);
828+
}
838829

839-
if(options.get_bool_option("string-abstraction"))
840-
{
841-
log.status() << "String Abstraction" << messaget::eom;
842-
string_abstraction(goto_model, log.get_message_handler());
843-
}
830+
if(options.get_bool_option("string-abstraction"))
831+
{
832+
log.status() << "String Abstraction" << messaget::eom;
833+
string_abstraction(goto_model, log.get_message_handler());
834+
}
844835

845-
// add failed symbols
846-
// needs to be done before pointer analysis
847-
add_failed_symbols(goto_model.symbol_table);
836+
// add failed symbols
837+
// needs to be done before pointer analysis
838+
add_failed_symbols(goto_model.symbol_table);
848839

849-
// recalculate numbers, etc.
850-
goto_model.goto_functions.update();
840+
// recalculate numbers, etc.
841+
goto_model.goto_functions.update();
851842

852-
// add loop ids
853-
goto_model.goto_functions.compute_loop_numbers();
843+
// add loop ids
844+
goto_model.goto_functions.compute_loop_numbers();
854845

855-
if(options.get_bool_option("drop-unused-functions"))
856-
{
857-
// Entry point will have been set before and function pointers removed
858-
log.status() << "Removing unused functions" << messaget::eom;
859-
remove_unused_functions(goto_model, log.get_message_handler());
860-
}
846+
if(options.get_bool_option("drop-unused-functions"))
847+
{
848+
// Entry point will have been set before and function pointers removed
849+
log.status() << "Removing unused functions" << messaget::eom;
850+
remove_unused_functions(goto_model, log.get_message_handler());
851+
}
861852

862-
// remove skips such that trivial GOTOs are deleted and not considered
863-
// for coverage annotation:
864-
remove_skip(goto_model);
853+
// remove skips such that trivial GOTOs are deleted and not considered
854+
// for coverage annotation:
855+
remove_skip(goto_model);
865856

866-
// instrument cover goals
867-
if(options.is_set("cover"))
868-
{
869-
const auto cover_config = get_cover_config(
870-
options, goto_model.symbol_table, log.get_message_handler());
871-
if(instrument_cover_goals(
872-
cover_config, goto_model, log.get_message_handler()))
873-
return true;
874-
}
857+
// instrument cover goals
858+
if(options.is_set("cover"))
859+
{
860+
const auto cover_config = get_cover_config(
861+
options, goto_model.symbol_table, log.get_message_handler());
862+
if(instrument_cover_goals(
863+
cover_config, goto_model, log.get_message_handler()))
864+
return true;
865+
}
875866

876-
// label the assertions
877-
// This must be done after adding assertions and
878-
// before using the argument of the "property" option.
879-
// Do not re-label after using the property slicer because
880-
// this would cause the property identifiers to change.
881-
label_properties(goto_model);
867+
// label the assertions
868+
// This must be done after adding assertions and
869+
// before using the argument of the "property" option.
870+
// Do not re-label after using the property slicer because
871+
// this would cause the property identifiers to change.
872+
label_properties(goto_model);
882873

883-
// reachability slice?
884-
if(options.get_bool_option("reachability-slice-fb"))
885-
{
886-
log.status() << "Performing a forwards-backwards reachability slice"
887-
<< messaget::eom;
888-
if(options.is_set("property"))
889-
reachability_slicer(
890-
goto_model, options.get_list_option("property"), true);
891-
else
892-
reachability_slicer(goto_model, true);
893-
}
894-
895-
if(options.get_bool_option("reachability-slice"))
896-
{
897-
log.status() << "Performing a reachability slice" << messaget::eom;
898-
if(options.is_set("property"))
899-
reachability_slicer(goto_model, options.get_list_option("property"));
900-
else
901-
reachability_slicer(goto_model);
902-
}
874+
// reachability slice?
875+
if(options.get_bool_option("reachability-slice-fb"))
876+
{
877+
log.status() << "Performing a forwards-backwards reachability slice"
878+
<< messaget::eom;
879+
if(options.is_set("property"))
880+
reachability_slicer(
881+
goto_model, options.get_list_option("property"), true);
882+
else
883+
reachability_slicer(goto_model, true);
884+
}
903885

904-
// full slice?
905-
if(options.get_bool_option("full-slice"))
906-
{
907-
log.status() << "Performing a full slice" << messaget::eom;
908-
if(options.is_set("property"))
909-
property_slicer(goto_model, options.get_list_option("property"));
910-
else
911-
full_slicer(goto_model);
912-
}
886+
if(options.get_bool_option("reachability-slice"))
887+
{
888+
log.status() << "Performing a reachability slice" << messaget::eom;
889+
if(options.is_set("property"))
890+
reachability_slicer(goto_model, options.get_list_option("property"));
891+
else
892+
reachability_slicer(goto_model);
893+
}
913894

914-
// remove any skips introduced since coverage instrumentation
915-
remove_skip(goto_model);
895+
// full slice?
896+
if(options.get_bool_option("full-slice"))
897+
{
898+
log.status() << "Performing a full slice" << messaget::eom;
899+
if(options.is_set("property"))
900+
property_slicer(goto_model, options.get_list_option("property"));
901+
else
902+
full_slicer(goto_model);
916903
}
917904

905+
// remove any skips introduced since coverage instrumentation
906+
remove_skip(goto_model);
907+
918908
return false;
919909
}
920910

0 commit comments

Comments
 (0)