36 auto vs_object_factory =
45 std::unique_ptr<ai_history_factory_baset> hf =
nullptr;
48 hf = std::make_unique<
53 hf = std::make_unique<call_stack_history_factoryt>(
58 hf = std::make_unique<local_control_flow_history_factoryt>(
65 std::unique_ptr<ai_domain_factory_baset> df =
nullptr;
68 df = std::make_unique<
73 df = std::make_unique<
78 df = std::make_unique<variable_sensitivity_domain_factoryt>(
79 vs_object_factory, vsd_config);
86 std::unique_ptr<ai_storage_baset> st =
nullptr;
89 st = std::make_unique<history_sensitive_storaget>();
93 st = std::make_unique<location_sensitive_storaget>();
98 if(hf !=
nullptr && df !=
nullptr && st !=
nullptr)
102 return std::make_unique<ai_recursive_interproceduralt>(
103 std::move(hf), std::move(df), std::move(st), mh);
110 return std::make_unique<ai_three_way_merget>(
111 std::move(hf), std::move(df), std::move(st), mh);
121 return std::make_unique<constant_propagator_ait>(
126 return std::make_unique<dependence_grapht>(ns, mh);
130 return std::make_unique<variable_sensitivity_dependence_grapht>(
131 goto_model.
goto_functions, ns, vs_object_factory, vsd_config, mh);
135 auto df = std::make_unique<variable_sensitivity_domain_factoryt>(
136 vs_object_factory, vsd_config);
137 return std::make_unique<ait<variable_sensitivity_domaint>>(std::move(df));
141 return std::make_unique<ait<interval_domaint>>();
147 return std::make_unique<ait<non_null_domaint> >();
159 return std::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.
Track function-local control flow for loop unwinding and path senstivity.
There are different ways of handling arrays, structures, unions and pointers.