@@ -446,6 +446,9 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
446
446
const optionst &options,
447
447
const namespacet &ns)
448
448
{
449
+ auto vsd_config = vsd_configt::from_options (options);
450
+ auto vs_object_factory = variable_sensitivity_object_factoryt::configured_with (vsd_config);
451
+
449
452
// These support all of the option categories
450
453
if (
451
454
options.get_bool_option (" recursive-interprocedural" ) ||
@@ -485,10 +488,6 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
485
488
}
486
489
else if (options.get_bool_option (" vsd" ))
487
490
{
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
-
492
491
df = util_make_unique<
493
492
variable_sensitivity_domain_factoryt>(vs_object_factory);
494
493
}
@@ -540,19 +539,11 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
540
539
}
541
540
else if (options.get_bool_option (" dependence-graph-vs" ))
542
541
{
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
-
547
542
return new variable_sensitivity_dependence_grapht (
548
543
goto_model.goto_functions , ns, vs_object_factory);
549
544
}
550
545
else if (options.get_bool_option (" vsd" ))
551
546
{
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
-
556
547
auto df = util_make_unique<variable_sensitivity_domain_factoryt>(vs_object_factory);
557
548
return new ait<variable_sensitivity_domaint>(std::move (df));
558
549
}
@@ -770,18 +761,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
770
761
771
762
if (options.get_bool_option (" general-analysis" ))
772
763
{
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
-
785
764
// Output file factory
786
765
const std::string outfile=options.get_option (" outfile" );
787
766
@@ -802,7 +781,17 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
802
781
// Build analyzer
803
782
log.status () << " Selecting abstract domain" << messaget::eom;
804
783
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
+ }
806
795
807
796
if (analyzer == nullptr )
808
797
{
0 commit comments