CBMC
build_analyzer.h File Reference
#include <memory>
+ Include dependency graph for build_analyzer.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

std::unique_ptr< ai_basetbuild_analyzer (const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
 Build an abstract interpreter configured by the options. More...
 

Function Documentation

◆ build_analyzer()

std::unique_ptr<ai_baset> build_analyzer ( const optionst options,
const goto_modelt goto_model,
const namespacet ns,
message_handlert mh 
)

Build an abstract interpreter configured by the options.

This may require options for:

  • which interpreter to use
  • which history to use
  • which storage to use
  • which domain to use
  • how that domain is configured Not every combination of options is supported. Unsupported options will give null. Domains also may throw a invalid_command_line_argument_exceptiont

Build an abstract interpreter configured by the options.

However at the moment some domains require the goto_model or parts of it

Definition at line 29 of file build_analyzer.cpp.