37 auto vs_object_factory =
46 std::unique_ptr<ai_history_factory_baset> hf =
nullptr;
54 hf = util_make_unique<call_stack_history_factoryt>(
59 hf = util_make_unique<local_control_flow_history_factoryt>(
66 std::unique_ptr<ai_domain_factory_baset> df =
nullptr;
79 df = util_make_unique<variable_sensitivity_domain_factoryt>(
80 vs_object_factory, vsd_config);
87 std::unique_ptr<ai_storage_baset> st =
nullptr;
90 st = util_make_unique<history_sensitive_storaget>();
94 st = util_make_unique<location_sensitive_storaget>();
99 if(hf !=
nullptr && df !=
nullptr && st !=
nullptr)
103 return util_make_unique<ai_recursive_interproceduralt>(
104 std::move(hf), std::move(df), std::move(st), mh);
111 return util_make_unique<ai_three_way_merget>(
112 std::move(hf), std::move(df), std::move(st), mh);
122 return util_make_unique<constant_propagator_ait>(
127 return util_make_unique<dependence_grapht>(ns);
131 return util_make_unique<variable_sensitivity_dependence_grapht>(
132 goto_model.
goto_functions, ns, vs_object_factory, vsd_config, mh);
136 auto df = util_make_unique<variable_sensitivity_domain_factoryt>(
137 vs_object_factory, vsd_config);
138 return util_make_unique<ait<variable_sensitivity_domaint>>(std::move(df));
142 return util_make_unique<ait<interval_domaint>>();
148 return util_make_unique<ait<non_null_domaint> >();
160 return util_make_unique<dependence_grapht>(ns);
std::unique_ptr< ai_baset > build_analyzer(const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
Ideally this should be a pure function of options.
History for tracking the call stack and performing interprocedural analysis.
An easy factory implementation for histories that don't need parameters.
goto_functionst goto_functions
GOTO functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
unsigned int get_unsigned_int_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
static variable_sensitivity_object_factory_ptrt configured_with(const vsd_configt &options)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Track function-local control flow for loop unwinding and path senstivity.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
static vsd_configt from_options(const optionst &options)
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
A forked and modified version of analyses/dependence_graph.
There are different ways of handling arrays, structures, unions and pointers.
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...