@@ -446,6 +446,9 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
446446 const optionst &options,
447447 const namespacet &ns)
448448{
449+ auto vsd_config = vsd_configt::from_options (options);
450+ auto vs_object_factory = variable_sensitivity_object_factoryt::configured_with (vsd_config);
451+
449452 // These support all of the option categories
450453 if (
451454 options.get_bool_option (" recursive-interprocedural" ) ||
@@ -485,10 +488,6 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
485488 }
486489 else if (options.get_bool_option (" vsd" ))
487490 {
488- auto vsd_config = vsd_configt::from_options (options);
489- auto vs_object_factory =
490- std::make_shared<variable_sensitivity_object_factoryt>(vsd_config);
491-
492491 df = util_make_unique<
493492 variable_sensitivity_domain_factoryt>(vs_object_factory);
494493 }
@@ -540,19 +539,11 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
540539 }
541540 else if (options.get_bool_option (" dependence-graph-vs" ))
542541 {
543- auto vsd_config = vsd_configt::from_options (options);
544- auto vs_object_factory =
545- std::make_shared<variable_sensitivity_object_factoryt>(vsd_config);
546-
547542 return new variable_sensitivity_dependence_grapht (
548543 goto_model.goto_functions , ns, vs_object_factory);
549544 }
550545 else if (options.get_bool_option (" vsd" ))
551546 {
552- auto vsd_config = vsd_configt::from_options (options);
553- auto vs_object_factory =
554- std::make_shared<variable_sensitivity_object_factoryt>(vsd_config);
555-
556547 auto df = util_make_unique<variable_sensitivity_domain_factoryt>(vs_object_factory);
557548 return new ait<variable_sensitivity_domaint>(std::move (df));
558549 }
@@ -770,18 +761,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
770761
771762 if (options.get_bool_option (" general-analysis" ))
772763 {
773- // TODO : replace with the domain factory infrastructure
774- // try
775- // {
776- // variable_sensitivity_object_factoryt::instance().set_options(
777- // vsd_configt::from_options(options));
778- // }
779- // catch(const invalid_command_line_argument_exceptiont &e)
780- // {
781- // log.error() << e.what() << messaget::eom;
782- // return CPROVER_EXIT_USAGE_ERROR;
783- // }
784-
785764 // Output file factory
786765 const std::string outfile=options.get_option (" outfile" );
787766
@@ -802,7 +781,17 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
802781 // Build analyzer
803782 log.status () << " Selecting abstract domain" << messaget::eom;
804783 namespacet ns (goto_model.symbol_table ); // Must live as long as the domain.
805- std::unique_ptr<ai_baset> analyzer (build_analyzer (options, ns));
784+ std::unique_ptr<ai_baset> analyzer;
785+
786+ try
787+ {
788+ analyzer.reset (build_analyzer (options, ns));
789+ }
790+ catch (const invalid_command_line_argument_exceptiont &e)
791+ {
792+ log.error () << e.what () << messaget::eom;
793+ return CPROVER_EXIT_USAGE_ERROR;
794+ }
806795
807796 if (analyzer == nullptr )
808797 {
0 commit comments