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.
Track function-local control flow for loop unwinding and path senstivity.
There are different ways of handling arrays, structures, unions and pointers.